Issue No. 02 - March-April (2007 vol. 24)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/MDT.2007.38
Sandip Ray , University of Texas at Austin
Rob Sumners , Advanced Micro Devices
This article presents a procedure for proving invariants of infinite-state reactive systems using a combination of two formal verification techniques: theorem proving and model checking. This method uses term rewriting on the definition of the target system to reduce an invariant proof of the target system to a reachability analysis on a finite predicate abstraction, which can be discharged through model checking. The method affords substantial automation in invariant proofs, while preserving the expressiveness and control afforded by theorem proving. The authors discuss how their approach enables the two disparate techniques, theorem proving and model checking, to complement one another. The procedure has been interfaced with the ACL2 theorem prover, and the authors describe its use in verifying cache coherence protocols in ACL2.
theorem proving, model checking, predicate abstraction, formal verification, ACL2
S. Ray and R. Sumners, "Combining Theorem Proving with Model Checking through Predicate Abstraction," in IEEE Design & Test of Computers, vol. 24, no. , pp. 132-139, 2007.