Sciweavers

CAV
2004
Springer

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

13 years 7 months ago
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...
Kedar S. Namjoshi
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where CAV
Authors Kedar S. Namjoshi
Comments (0)