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


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",
}