Proving Invariants via Rewriting and Abstraction

R. Sumners and S. Ray

Technical Report TR-05-35, Department of Computer Sciences, University of Texas at Austin, July 2005.

Abstract

We present a deductive method for proving invariants of reactive systems. Our approach uses term rewriting to reduce invariant proofs to reachability analysis on a finite graph. This substantially automates invariant proofs by obviating the need to define inductive invariants while still benefitting from the expressiveness of deductive methods. We implement a procedure supporting this approach which interfaces with the ACL2 theorem prover. The interface affords sound extension of our procedure with rewrite rules based on proven theorems. We demonstrate the method in the verification of cache coherence protocols.

Relevant files