The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.02 - March-April (2007 vol.24)
pp: 132-139
Sandip Ray , University of Texas at Austin
Rob Sumners , Advanced Micro Devices
ABSTRACT
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.
INDEX TERMS
theorem proving, model checking, predicate abstraction, formal verification, ACL2
CITATION
Sandip Ray, Rob Sumners, "Combining Theorem Proving with Model Checking through Predicate Abstraction", IEEE Design & Test of Computers, vol.24, no. 2, pp. 132-139, March-April 2007, doi:10.1109/MDT.2007.38
18 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool