Software Tools for Technology Transfer manuscript No. (will be inserted by the editor) Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC

The date of receipt and acceptance will be inserted by the editor 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 in-tended way. While vacuity detection is effective, it is a rela-tively expensive technique requiring many additional model-checking runs. We address the problem of efficient vacuity detection for Bounded Model Checking (BMC) of LTL prop-erties, 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 character-istic of resolution proofs – peripherality – and prove that if a variable is a source of vacuity, then there exists a resolu-tion proof in which this variable is peripheral. Our vacuity detection tool, VaqTree, uses these methods to detect vacu-ous variables, decreasing the total number of model-checking runs required to detect all sources of vacuity.