Abstract: The success of model checking for large programs depends crucially on the ability to efficiently construct abstractions that track only the small set of facts relevant to the property being verified. The Counterexample-Guided Abstraction Refinement (CEGAR) paradigm provides an attractive strategy for finding such a set of facts -- iteratively refine a coarse set using counterexamples, until either the property is proved or refuted.

To apply this paradigm, we must answer the following basic questions:
1. How can we use a counterexample to find relevant facts ?
2. How can we efficiently approximate program behaviors using a given set of facts ?
3. How can we select facts to ensure that the iterative refinement is complete ?

In this talk, we describe a solution to these three problems that is based upon the insight that program behaviors can be encoded as logical formulas whose proofs of unsatisfiability can be efficiently mined to extract Craig Interpolants which capture exactly the information relevant to verification.

First, we describe how the interpolants yield relevant facts and can be used to precisely and efficiently approximate the transition relation. Next, we describe how interpolants can be computed from appropriately structured proofs, and how the structure of the proof ensures that the iterative-refinement loop is complete. We conclude by describing how BLAST uses abstractions from unsatisfiability proofs to verify a variety of programs that were previously beyond the scope of automatic software model checkers. (Joint work with Tom Henzinger, Rupak Majumdar and Ken McMillan)

Ranjit Jhala is an Assistant Professor in the Department of Computer Science and Engineering at UC San Diego. Before joining UCSD, he was a graduate student at UC Berkeley. Ranjit is interested in Programming Languages and Software Engineering, more specifically, in techniques for building reliable computer systems. His work draws from, combines and contributes to methods the areas of Model Checking, Program Analysis and Automated Deduction, e.g. the application of ideas from software model checking to automatically infer dependent types for ML. Appointments: dcm@cs.cmu.edu