file.pdf (166.23 kB)
Download fileConstructing Quantified Invariants via Predicate Abstraction
journal contribution
posted on 01.01.1976, 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 where the system state contains mutable
function and predicate state variables. 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 function
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 with unbounded
FIFO channels.