Equational abstractions

DOI10.1016/J.TCS.2008.04.040MaRDI QIDQ944377zbMATH OpenOpenAlexWikidataFDO

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

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 checkingLTLrewriting logicalgebraic specificationMaudeabstractions

Mathematics Subject Classification ID

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

Recommendations

• Automated Deduction – CADE-19
• Equational abstractions in rewriting logic and Maude
• Abstraction and abstraction refinement
• scientific article; zbMATH DE number 2110619
• scientific article; zbMATH DE number 2102725

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 3970817 (Why is no real title available?)
• scientific article; zbMATH DE number 1189278 (Why is no real title available?)
• scientific article; zbMATH DE number 3703962 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 2038715 (Why is no real title available?)
• scientific article; zbMATH DE number 2102725 (Why is no real title available?)
• A new solution of Dijkstra's concurrent programming problem
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
• Characterizing finite Kripke structures in propositional temporal logic
• Conditional rewriting logic as a unified model of concurrency
• Control and data abstraction: The cornerstones of practical formal verification
• ELAN from a rewriting logic point of view
• Equational rules for rewriting logic
• Maude: specification and programming in rewriting logic
• On the desirability of mechanizing calculational proofs
• Recent Trends in Algebraic Development Techniques
• Specification and proof in membership equational logic
• The Maude LTL model checker
• Verification by augmented finitary abstraction

Cited in

(20)

• Generalized rewrite theories, coherence completion, and symbolic methods
• Twenty years of rewriting logic
• Equational formulas and pattern operations in initial order-sorted algebras
• Building correct-by-construction systems with formal patterns
• Automated Deduction – CADE-19
• Model checking TLR* guarantee formulas on infinite systems
• Equational abstractions in rewriting logic and Maude
• On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
• Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
• Optimizing Maude programs via program specialization
• Symbolic Specialization of Rewriting Logic Theories with Presto
• Abstraction in fixpoint logic
• Automatic verification of reduction techniques in higher order logic
• Algebraic simulations
• Programming and symbolic computation in Maude
• Optimization of rewrite theories by equational partial evaluation
• Quotient dynamics: the logic of abstraction
• Termination criteria for tree automata completion
• Language definitions as rewrite theories
• Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs

Describes a project that uses

Uses Software

• ITP
• MTT
• Maude
• CafeOBJ

This page was built for publication: Equational abstractions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q944377)