Sciweavers

FMCAD
2007
Springer

Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC

14 years 4 months ago
Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC
—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 partial 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.
Jocelyn Simmonds, Jessica Davies, Arie Gurfinkel,
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where FMCAD
Authors Jocelyn Simmonds, Jessica Davies, Arie Gurfinkel, Marsha Chechik
Comments (0)