Before And After Vacuity

摘要

In formal verification, we verify that a system is correct with respect to a specification. Cases like antecedent failure can make a successful pass of the verification procedure meaningless. Vacuity detection can signal such "meaningless" passes of the specification, and indeed vacuity checks are now a standard component in many commercial model checkers. We address two dimensions of vacuity: the computational effort and the information that is given to the user. As for the first dimension, we present several preliminary vacuity checks that can be done without the design itself, which implies that some information can be found with a significantly smaller effort. As for the second dimension, we present algorithms for deriving two types of information that are not provided by standard vacuity checks, assuming M (=) p for a model M and formula p: (a) behaviors that are possibly missing from M (or wrongly restricted by the environment) (b) the largest subset of occurrences of literals in p that can be replaced with FALSE simultaneously without falsifying p in M. The complexity of each of these problems is proven. Overall this extra information can lead to tighter specifications and more guidance for finding errors.