Combining Theorem Proving with Model Checking through Predicate Abstraction

S. Ray and R. Sumners

IEEE Design & Test of Computers, volume 24(2) March-April 2007 (Special Issue on Advances in Functional Validation through Hybrid Techniques), pages 132-139. IEEE Computer Society.

© 2007 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

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. We 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 we describe its use in verifying cache coherence protocols in ACL2.

Relevant files

Paper (pdf)

BibTex

@Article{ray-combining,
  author    = "S. Ray and R. Sumners",
  title     = "{Combining Theorem Proving with Model Checking Through Predicate Abstraction}",
  journal   = "{IEEE Design \& Test of Computers}",
  volume    = "24",
  number    = "2",
  pages     = "132-139",
  publisher = "{IEEE Computer Society}",
  year      = "2007"
}