file.pdf (298.9 kB)
Predicate Abstraction with Indexed Predicates
journal contribution
posted on 1989-01-01, 00:00 authored by Shuvendu K. Lahiri, Randal E. BryantPredicate abstraction provides a powerful tool for verifying properties of infinite-state systems
using a combination of a decision procedure for a subset of first-order logic and symbolic methods
originally developed for finite-state model checking.We consider models containing first-order state
variables, where the system state includes mutable functions and predicates. Such a model can
describe systems containing arbitrarily large memories, buffers, and arrays of identical processes.
We describe a form of predicate abstraction that constructs a formula over a set of universally
quantified variables to describe invariant properties of the first-order state variables. We provide
a formal justification of the soundness of our approach and describe how it has been used to verify
several hardware and software designs, including a directory-based cache coherence protocol.