Paper Info
Title
Constructing Quantified Invariants via Predicate Abstraction
Abstract
Predicate 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.
Year
DOI
Venue
2004
10.1007/978-3-540-24622-0_22
Lecture Notes in Computer Science
Keywords
Field
DocType
model checking,first order logic,software design
Predicate variable,Model checking,Predicate abstraction,Computer science,Finite-state machine,Theoretical computer science,First-order logic,Functional predicate,True quantified Boolean formula,Predicate (mathematical logic)
Conference
Volume
ISSN
Citations 
2937
0302-9743
46
PageRank 
References 
Authors
2.15
11
2
Name
Order
Citations
PageRank
Shuvendu K. Lahiri1142468.18
Randal E. Bryant292041194.64