# 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

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