Equational abstractions

DOI10.1016/j.tcs.2008.04.040zbMath1155.68050OpenAlexW2913689616WikidataQ123905877 ScholiaQ123905877MaRDI QIDQ944377

Miguel Palomino, Narciso Martí-Oliet, José Meseguer

Publication date: 16 September 2008

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2008.04.040

zbMATH Keywords

model checkingalgebraic specificationLTLrewriting logicMaudeabstractions

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Temporal logic (03B44)

Related Items

Equational formulas and pattern operations in initial order-sorted algebras ⋮ Algebraic simulations ⋮ Optimization of rewrite theories by equational partial evaluation ⋮ Verifying Reachability-Logic Properties on Rewriting-Logic Specifications ⋮ Twenty years of rewriting logic ⋮ On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories ⋮ Symbolic Specialization of Rewriting Logic Theories with Presto ⋮ Optimizing Maude programs via program specialization ⋮ Automatic verification of reduction techniques in higher order logic ⋮ Model Checking TLR* Guarantee Formulas on Infinite Systems ⋮ Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs ⋮ Equational Abstractions in Rewriting Logic and Maude ⋮ Termination criteria for tree automata completion ⋮ Language definitions as rewrite theories ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Programming and symbolic computation in Maude

Uses Software

• CafeOBJ
• Maude
• MTT
• ITP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Characterizing finite Kripke structures in propositional temporal logic
• Conditional rewriting logic as a unified model of concurrency
• On the desirability of mechanizing calculational proofs
• ELAN from a rewriting logic point of view
• Maude: specification and programming in rewriting logic
• Equational rules for rewriting logic
• Verification by augmented finitary abstraction
• Control and data abstraction: The cornerstones of practical formal verification
• Specification and proof in membership equational logic
• A new solution of Dijkstra's concurrent programming problem
• Recent Trends in Algebraic Development Techniques