Before and after vacuity

Hana Chockler, Ofer Strichman*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

9 Citations (Scopus)

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 two types of information that are not provided by standard vacuity checks, assuming M satisfies phi for a model M and formula phi: (a) behaviors that are possibly missing from M (or wrongly restricted by the environment) (b) the largest subset of occurrences of literals in. that can be replaced with FALSE simultaneously without falsifying. 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.

Original languageEnglish
Pages (from-to)37-58
Number of pages22
JournalFORMAL METHODS IN SYSTEM DESIGN
Volume34
Issue number1
DOIs
Publication statusPublished - Feb 2009

Keywords

  • COVERAGE METRICS
  • Complexity
  • MODEL CHECKING
  • Vacuity
  • COMPLEXITY
  • Model-checking

Fingerprint

Dive into the research topics of 'Before and after vacuity'. Together they form a unique fingerprint.

Cite this