Name
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 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. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1145/1297658.1297662 | ACM Transactions on Computational Logic (TOCL) |
Keywords | DocType | Volume |
cache-coherence protocols,system state,directory-based cache coherence protocol,decision procedure,invariant synthesis,abstract interpretation,first-order state variable,innite-state veri- cation,formal justification,formal verification,additional key words and phrases: formal verication,predicate abstraction,infinite-state verification,finite-state model checking,infinite-state system,identical process,first-order logic,software design,indexation,model checking | Journal | 9 |
Issue | ISSN | Citations |
1 | 1529-3785 | 27 |
PageRank | References | Authors |
1.03 | 29 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Shuvendu K. Lahiri | 1 | 1424 | 68.18 |
| Randal E. Bryant | 2 | 9204 | 1194.64 |