Abstract: Model Checking and (Deductive) Proof Checking are regarded as being quite different approaches to program verification. In this talk, I will describe close connections between the two, with the connecting “glue” provided by abstraction.

In the first part of the talk, I show how to create a “certifying” model checker, one which can produce an independently checkable proof (the certificate) to justify the computed answer. This capability enables many applications, including proof carrying code, vacuity detection, and incremental model checking.

In the second half of the talk, I consider the following “completeness” question: does model checking (coupled with abstraction) suffice to show correctness? The answer is based on a transformation that takes a correctness proof to an abstraction function. Along the way, I show the surprising fact that the well-studied May-Must abstraction framework is incomplete for branching-time properties, and propose a remedy.

The talk is reasonably self-contained, but I do assume some familiarity with model checking and CTL. The talk is based in part on work done together with Dennis Dams.

Kedar Namjoshi is a member of the Computing Sciences Research Center at Bell Laboratories. He holds an M.S. and a Ph.D. in Computer Sciences from the University of Texas at Austin, and a B.Tech. degree in Computer Science and Engineering from the Indian Institute of Technology, Madras. His research interests span the theory and practice of program verification, including temporal logic, model checking, deductive methods, and static code analysis.