Easier and More Informative Vacuity Checks

Hana Chockler, Ofer Strichman

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

24 Citations (Scopus)
75 Downloads (Pure)

Abstract

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 three types of information that are not provided by standard vacuity checks, assuming M \= phi for a model M and property phi: a) behaviors that are possibly missing from M (or wrongly restricted by the environment) b) the largest subset of occurrences of literals in phi that can be replaced with false simultaneously without falsifying phi in M, and finally c) the degree of responsibility of each occurrence of a literal in phi to its satisfaction in the model M, which can be seen as a fine-grain form of vacuity. The complexity of each of these problems is proven. Overall this extra information can lead to tighter specifications and more guidance for finding errors.
Original languageEnglish
Title of host publicationProceedings of ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE)
PublisherIEEE Computer Society
Pages189-198
Number of pages10
Publication statusPublished - 30 May 2007

Fingerprint

Dive into the research topics of 'Easier and More Informative Vacuity Checks'. Together they form a unique fingerprint.

Cite this