Sanity Checks in Formal Verification

One of the advantages of temporal-logic model-checking tools is their
ability to accompany a negative answer to the correctness query by a
counterexample to the satisfaction of the specification in the system.
On the other hand, when the answer to the correctness query is
positive, most model-checking tools provide no additional
information. In the last few years there has been growing awareness to
the importance of suspecting the system or the specification of
containing an error also in the case model checking succeeds. The main
justification of such suspects are possible errors in the modeling of
the system or of the specification.  The goal of sanity checks is to
detect such errors by further automatic reasoning.  Two leading sanity
checks are {\em vacuity\/} and {\em coverage}.  In vacuity, the goal
is to detect cases where the system satisfies the specification in
some unintended trivial way. In coverage, the goal is to increase the
exhaustiveness of the specification by detecting components of the
system that do not play a role in verification process. For both
checks, the challenge is to define vacuity and coverage formally,
develop algorithms for detecting vacuous satisfaction and low
coverage, and suggest methods for returning to the user helpful
information. We survey existing work on vacuity and coverage and argue
that, in many aspects, the two checks are essentially the same: both
are based on repeating the verification process on some mutant
input. In vacuity, mutations are in the specifications, whereas in
coverage, mutations are in the system. This observation enables us to
adopt work done in the context of vacuity to coverage, and vise versa.