Relevance Heuristics for Program Analysis

March 5, 2009
Ken McMillan | Cadence Research Labs

Relevance heuristics allow us to tailor a program analysis to a particular property to be verified. This in turn makes it possible to improve the precision of the analysis where needed, while maintaining scalability. In this talk I will discuss the principles by which SAT solvers and other decision procedures decide what information is relevant to a given proof. Then we will see how these ideas can be exploited in program verification using the method of Craig interpolation. The result is an analysis that is finely tuned to prove a given property of a program. At the end of the talk, I will cover some recent research in this area, including the use of interpolants for verifying heap-manipulating programs.

Speaker Details

Ken McMillan is a fellow at Cadence Research Labs in Berkeley, California. He works in formal verification, primarily in model checking for hardware and software. He holds a BS in electrical engineering from the University of Illinois at Urbana (1984), an MS in electrical engineering from Stanford (1986) and a Ph.D. in computer science from Carnegie Mellon (1992). He is the author of the book “Symbolic Model Checking”, and the SMV symbolic model checking system.For his work on symbolic model checking, he received the 1992 ACM doctoral dissertation award, the SRC technical excellence award, the ACM Paris Kannelakis award, and the Alan Newell award from Carnegie Mellon.