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.
