Invariant-driven specifications in Maude

DOI10.1016/J.SCICO.2009.03.003MaRDI QIDQ838161zbMATH OpenOpenAlexFDO

Authors Manuel Roldán, Francisco Durán, Antonio Vallecillo

Publication date 21 August 2009

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.scico.2009.03.003

zbMATH Keywords

invariantsreflectionrewriting logicexecution strategiesmaude

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Maude: specification and programming in rewriting logic
• Strategies and user interfaces in Maude at work
• Strategies, Model Checking and Branching-Time Properties in Maude
• Parameterized strategies specification in Maude
• Membrane Computing

Cites work

• scientific article; zbMATH DE number 1722718 (Why is no real title available?)
• scientific article; zbMATH DE number 5668423 (Why is no real title available?)
• scientific article; zbMATH DE number 4074535 (Why is no real title available?)
• scientific article; zbMATH DE number 1189278 (Why is no real title available?)
• scientific article; zbMATH DE number 42431 (Why is no real title available?)
• scientific article; zbMATH DE number 46957 (Why is no real title available?)
• scientific article; zbMATH DE number 1231664 (Why is no real title available?)
• scientific article; zbMATH DE number 1946735 (Why is no real title available?)
• scientific article; zbMATH DE number 2085181 (Why is no real title available?)
• scientific article; zbMATH DE number 2087521 (Why is no real title available?)
• scientific article; zbMATH DE number 1569132 (Why is no real title available?)
• scientific article; zbMATH DE number 910719 (Why is no real title available?)
• Algebraic Methodology and Software Technology
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Conditional rewriting logic as a unified model of concurrency
• ELAN from a rewriting logic point of view
• Maude's module algebra
• Maude: specification and programming in rewriting logic
• Real-time logics: Complexity and expressiveness
• Structured theories and institutions
• The B-Book
• The Maude LTL model checker

Cited in

(4)

• Mechanizing invariant proofs of joint action systems
• Debugging Maude programs via runtime assertion checking and trace slicing
• Combining runtime checking and slicing to improve Maude error diagnosis
• Safety enforcement via programmable strategies in Maude

Describes a project that uses

Uses Software

• Jaza
• KeY
• Z2sal
• Maude
• OBJ3
• SPIN
• Stratego

This page was built for publication: Invariant-driven specifications in Maude

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