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

Model checking algorithms can report a property as being true for reasons that may be considered vacuous. Current algorithms for detecting vacuity require either checking a quadratic size witness formula, or multiple model checking runs; either alternative may be quite expensive in practice. Vacuity is, in its essence, a problem with the justification used 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 extracted from the model checker in the form of an automatically generated proof. This check requires a small amount of computation after a single verification run on the property, so it is significantly more efficient than the earlier methods. While the new formulation is stronger, and so reports vacuity less often, we show that it agrees with the current formulations...

• Type: Conference
• Year: 2004
• Where: CAV
• Authors: Kedar S. Namjoshi
• Keywords: CAV 2004, Hardware, Model Checker, Model Checking, Model Checking Algorithms