Abstract

We present an approach based on inductive theorem proving for verifying invari- ants of dynamic systems specified in rewriting logic, a formal specification language imple- mented in the Maude system. An invariant is a property that holds on all the states that are reachable from a given class of initial states. Our approach consists in encoding the semantic aspects that are relevant for our task (namely, verifying invariance properties of the specified systems) in membership equational logic, a sublogic of rewriting logic. The invariance prop- erties are then formalized over the encoded rewrite theories and are proved using an inductive theorem prover for membership equational logic also implemented in the Maude system using its reflective capabilities. We illustrate our approach by verifying mutual exclusion properties of a readers-writers system and of an n-process version of the Bakery algorithm.