Experience with Predicate Abstraction

ion ? Satyaki Das 1 , David L. Dill 1 , and Seungjoon Park 2 1 Computer Systems Laboratory, Stanford University, Stanford, CA 94305 2 RIACS, NASA Ames Research Center, Moffett Field, CA 94035 Abstract. 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 using a language of iterated guarded commands, called MurOE \Gamma\Gamma (since it is a simplified version of our MurOE protocol description language). The system makes use of two libraries: SVC [1] (an efficient decision procedure for quantifierfree 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 appl..