Vacuity detection is a common practice accompanying model checking of hardware designs. Roughly speaking, a system satisfies a specification vacuously if it can satisfy a stronger specification obtained by replacing some of its subformulas with stronger expressions. If this happens then part of the specification is immaterial, which typically indicates that there is a problem in the model or the specification itself.
|Title of host publication||Verification, Model Checking, and Abstract Interpretation|
|Editors||Ahmed Bouajjani, David Monniaux|
|Place of Publication||Cham|
|Publisher||Springer International Publishing AG|
|Number of pages||18|
|Publication status||Published - 2017|