An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking

Model checking algorithms may sometimes report a property as being true for reasons that can be considered vacuous. Current algorithms for detecting the vacuous varification of a correctness property require either the generation of a quadratic size witness formula, or several model checking runs, either alternative may be quite expensive in practice. Vacuity is, in its essence, a problem with the justification given by the model checker for deeming the property to be true. We argue that current definitions of vacuity are too broad from this perspective, and give a new, narrower, formulation. The new formulation leads to a simple detection method that examines only the justification produced by the model checker for the verification, which is in the form of an automatically generated proof.