Experience with Predicate Abstraction
- 1 January 1999
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 160-171
- https://doi.org/10.1007/3-540-48683-6_16
Abstract
This reports some experiences with a recently-implemented prototype system for verification using predicate abstraction, based on the method of Graf and Saïdi [ 9 ]. Systems are described using a language of iterated guarded commands, called Murø-- (since it is a simplified version of our Murø protocol description language). The system makes use of two libraries: SVC [ 1 ] (an efficient decision procedure for quantifier- free first-order logic) and the CMU BDD library. The use of these libraries increases the scope of problems that can be handled by predicate abstraction through increased efficiency, especially in SVC, which is typically called thousands of times. The verification system also provides limited support for quantifiers in formulas. The system has been applied successfully to two nontrivial examples: the Flash multiprocessor cache coherence protocol, and a concurrent garbage collection algorithm. Verification of the garbage collector algorithm required proving properties simple of graphs, which was also done using predicate abstraction.Keywords
This publication has 15 references indexed in Scilit:
- Verification of Cache Coherence Protocols by Aggregation of Distributed TransactionsTheory of Computing Systems, 1998
- Generating finite-state abstractions of reactive systems using decision proceduresPublished by Springer Science and Business Media LLC ,1998
- Construction of abstract state graphs with PVSLecture Notes in Computer Science, 1997
- Validity checking for combinations of theories with equalityPublished by Springer Science and Business Media LLC ,1996
- Temporal Verification of Reactive SystemsPublished by Springer Science and Business Media LLC ,1995
- Reasoning about ringsPublished by Association for Computing Machinery (ACM) ,1995
- Reasoning about systems with many processesJournal of the ACM, 1992
- An incremental garbage collection algorithm for multi-mutator systemsDistributed Computing, 1988
- Algorithms for on-the-fly garbage collectionACM Transactions on Programming Languages and Systems, 1984
- On-the-fly garbage collectionCommunications of the ACM, 1978