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