This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Combining Theorem Proving with Model Checking through Predicate Abstraction
March-April 2007 (vol. 24 no. 2)
pp. 132-139
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.
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
Usage of this product signifies your acceptance of the Terms of Use.