Abstract: Automated abstraction is a key technology in extending computer-aided verification methods to larger and more complex systems. In general terms, given a system and a property to prove, abstraction means extracting a simple set of facts about the system that are sufficient to prove the property. In this talk, we will see that this notion of abstraction is closely related to Craig's interpolation lemma. This is a classical result about predicate logic connecting proofs and abstraction. The lemma states that if formula A implies formula B, then there is an interpolant formula A' such that A implies A' and A' implies B, and such that A' is expressed over the common symbols of A and B. In some sense, the interpolant is an abstraction of A sufficient to prove B.

Given a proof that A implies B using resolution, we can derive an interpolant formula A' in linear time. This fact has a wide range of applications in model checking. For example, we can use it to build a very robust algorithm for model checking industrial hardware designs using just a Boolean satisfiability solver. In infinite-state verification, we can use interpolation to construct invariants, to derive suitable predicates for predicate abstraction, and to abstract transition behavior. This has led to orders-of-magnitude speed improvements in verifying device driver codes.

This talk will cover the basic theory behind the derivation of interpolants from proofs. We will consider how the form of the proof determines the form of the interpolant, and the implications of this for various applications, including the question of convergence. We will see that by controlling the structure of proofs, we can guarantee convergence to a fixed point proving a given property when one exists, even in an abstract lattice of infinite height.

Ken McMillan is a CMU alumnus, who got his Ph.D. in computer science in 1992, with Ed Clarke. He is currently a fellow at Cadence Berkeley Labs in Berkeley, California. He works in formal verification, primarily in model checking for hardware and software, and in compositional methods. He got his BS in electrical engineering from the University of Illinois at Urbana (1984), and MS in electrical engineering from Stanford (1986). He is the author of the book "Symbolic Model Checking", and the SMV symbolic model checking system. He has received the ACM doctoral dissertation award, the SRC technical excellence award, the ACM Paris Kannelakis award, and the Alan Newell award from Carnegie Mellon. He's always happy to get back to Pittsburgh and CMU. Appointments: dcm@cs.cmu.edu