Exploiting resolution proofs to speed up LTL vacuity detection for BMC

Abstract—When model-checking reports that a property holds on a model, vacuity detection increases user confidence in this result by checking that the property is satisfied in the intended way. While vacuity detection is effective, it is a relatively expensive technique requiring many additional model-checking runs. We address the problem of efficient vacuity detection for Bounded Model Checking (BMC) of LTL properties, presenting three par-tial vacuity detection methods based on the efficient analysis of the resolution proof produced by a successful BMC run. In particular, we define a characteristic of resolution proofs – peripherality – and prove that if a variable is a source of vacuity, then there exists a resolution proof in which this variable is peripheral. Our vacuity detection tool, VaqTree, uses these methods to detect vacuous variables, decreasing the total number of model-checking runs required to detect all sources of vacuity. I