TY - GEN
T1 - Proving safety properties of rewrite theories
AU - Rocha, Camilo
AU - Meseguer, José
PY - 2011
Y1 - 2011
N2 - Rewrite theories are a general and expressive formalism for specifying concurrent systems in which states are axiomatized by equations and transitions among states are axiomatized by rewrite rules. We present a deductive approach for verifying safety properties of rewrite theories in which all formal temporal reasoning about concurrent transitions is ultimately reduced to purely equational inductive reasoning. Narrowing modulo axioms is extensively used in our inference system to further simplify the equational proof obligations to which all proofs of safety formulas are ultimately reduced. In this way, existing equational reasoning techniques and tools can be directly applied to verify safety properties of concurrent systems. We report on the implementation of this deductive system in the Maude Invariant Analyzer tool, which provides a substantial degree of automation and can automatically discharge many proof obligations without user intervention.
AB - Rewrite theories are a general and expressive formalism for specifying concurrent systems in which states are axiomatized by equations and transitions among states are axiomatized by rewrite rules. We present a deductive approach for verifying safety properties of rewrite theories in which all formal temporal reasoning about concurrent transitions is ultimately reduced to purely equational inductive reasoning. Narrowing modulo axioms is extensively used in our inference system to further simplify the equational proof obligations to which all proofs of safety formulas are ultimately reduced. In this way, existing equational reasoning techniques and tools can be directly applied to verify safety properties of concurrent systems. We report on the implementation of this deductive system in the Maude Invariant Analyzer tool, which provides a substantial degree of automation and can automatically discharge many proof obligations without user intervention.
UR - http://www.scopus.com/inward/record.url?scp=80053034624&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-22944-2_22
DO - 10.1007/978-3-642-22944-2_22
M3 - Conference contribution
AN - SCOPUS:80053034624
SN - 9783642229435
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 314
EP - 328
BT - Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Proceedings
T2 - 4th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2011
Y2 - 30 August 2011 through 2 September 2011
ER -