Reducing Invariant Proofs to Finite Search via Rewriting

R. Sumners and S. Ray

In M. Kaufmann and J S. Moore, editors, 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004), Austin, TX, November 2004

Abstract

We present a tool-supported methodology for proving predicates invariant over all time for any behavior of a given system. We prove invariants by exploring a finite graph generated from the definition of the predicate using rewrite rules from proven ACL2 theorems. The methodology provides a means for proving invariants which avoids the complexity and cost of defining an inductive invariant while still allowing the proof of invariants for reactive systems modeled in an expressive language. We present two examples of the application of the methodology: a simple critical section example, and a slightly more complex ESI cache coherence model.

Relevant files

Paper (ps, pdf)
Slides for ACL2 2004 (ps, pdf)
Supporting materials: See the directory books/workshops/2004/sumners-ray/support/ in the current ACL2 distribution. (Note: You need the workshops tarball. See the instructions for installing ACL2 in the ACL2 homepage.)

BibTex

@Inproceedings{sumners-reducing,
  title     = "{Reducing Invariant Proofs to Finite Search via Rewriting}",
  author    = "R. Sumners and S. Ray",
  editor    = "M. Kaufmann and J S. Moore",
  booktitle = "{$5$th International Workshop on the ACL2 Theorem Prover and Its Applications
                (ACL2 2004)}",
  month     = nov,
  address   = "{Austin, TX}",
  year      = "2004",
}