Shuvendu Lahiri Carnegie Mellon University

A Symbolic Approach to Predicate Abstraction

Predicate abstraction is a useful form of abstraction for the verification of transition systems with large or infinite state spaces. One of the main bottlenecks of this approach is the extremely large number of decision procedures calls that are required to construct the abstract state space. In this talk, we propose the use of a symbolic decision procedure and its application for predicate abstraction. The advantage of the approach is that it reduces the number of calls to decision procedure exponentially and also provides for reducing the re-computations inherent in the current approaches. We will compare two implementations of the symbolic decision procedure: one based on BDDs which leverages the current advances in early quantification algorithms, and the other based on SAT-based quantifier elimination. We also demonstrate our approach with quantified predicates for verifying parameterized systems. We will illustrate the effectiveness of this approach on benchmarks from the verification of microprocessors, communication protocols, parameterized systems, and Microsoft Windows device drivers.

Bio
Shuvendu Lahiri is currently a Ph.D. candidate in the ECE department at CMU. He received his Masters in May 2001 working on Formal Verification with Prof. Randy Bryant. Earlier, he completed his B.Tech in Computer Science and Engineering at the Indian Institute of Technology at Kharagpur, India. His research interests include modeling and reasoning about systems with large or infinite state spaces. In this direction, he has worked on theorem provers for quantifier-free first-order logic, modeling and verification of microprocessors with out-of-order execution. Most recently, he is interested in applying predicate abstraction based techniques for reasoning about a variety of infinite-state systems.