Certifying Model Checkers

Model Checking is an algorithmic technique to determine whether a temporal property holds of a program. For linear time properties, if the check fails, most model checkers produce a counterexample computation. This computation can be viewed as a "certificate of badness", as it can be checked easily and independently of the model checker by simulating it on the program. On the other hand, no such certificate is produced if the check succeeds. In this paper, we show how this asymmetry can be eliminated with a certifying model checker. The key idea is that, if model checking is successful, a deductive proof of this fact can be generated with some extra effort. This proof acts as a "certificate of goodness", which can be checked mechanically by simple, non-fixpoint methods that are independent of the model checker. We develop a deductive proof system for verifying branching time properties expressed in the mu-calculus, and show how to generate a proof in this system from a successful model checking run. Proofs for linear time properties form a special case. A model checker that generates proofs can be used for many interesting applications. We discuss some of these, which include better ways of exploring errors in a program and tight integration of model checking with automatic theorem proving.