Experience with Predicate Abstraction

摘要: This reports some experiences with a recently-implemented prototype system for verification using predicate abstraction, based on the method of Graf and Saidi [9]. Systems are described language iterated guarded commands, called MurΦ-- (since it is simplified version our MurΦ protocol description language). The makes use two libraries: SVC [1] (an efficient decision procedure quantifier-free first-order logic) CMU BDD library. these libraries increases scope problems that can be handled by abstraction through increased efficiency, especially in SVC, which typically thousands times. also provides limited support quantifiers formulas. has been applied successfully to nontrivial examples: Flash multiprocessor cache coherence protocol, concurrent garbage collection algorithm. Verification collector algorithm required proving properties simple graphs, was done abstraction.