1999 | OriginalPaper | Buchkapitel
Experience with Predicate Abstraction
verfasst von : Satyaki Das, David L. Dill, Seungjoon Park
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.