Proving Safety Properties of Rewrite Theories

Rewriting logic theories are a general and expressive way of specifying concurrent systems, where states are axiomatized by equations and transitions among states are axiomatized by rewrite rules. In this paper, we present a {\em transformational} and {\em reductionistic} deductive approach for verifying {\em safety properties} of rewrite theories. In our approach all formal temporal reasoning about concurrent transitions is ultimately reduced to purely equational inductive reasoning. Narrowing modulo axioms is extensively used to simplify the equational proof obligations to which all proofs of safety formulas are ultimately reached. This allows these generic verification methods to take advantage of the existing wealth of equational reasoning techniques and tools already available. 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.unpublishednot peer reviewe