Space-Efficient Bounded Model Checking

TL;DR

This paper explores the use of Quantified Boolean Formulae (QBF) in bounded model checking to address memory issues, developing a specialized decision procedure and comparing it with existing methods on industrial benchmarks.

Contribution

It introduces a specialized QBF decision procedure for BMC and evaluates its effectiveness against general-purpose solvers on real-world benchmarks.

Findings

QBF-based BMC reduces memory usage compared to SAT-based methods.

The specialized QBF decision procedure outperforms general-purpose solvers in certain benchmarks.

QBF methods show promise for more scalable bounded model checking.

Abstract

Current algorithms for bounded model checking use SAT methods for checking satisfiability of Boolean formulae. These methods suffer from the potential memory explosion problem. Methods based on the validity of Quantified Boolean Formulae (QBF) allow an exponentially more succinct representation of formulae to be checked, because no "unrolling" of the transition relation is required. These methods have not been widely used, because of the lack of an efficient decision procedure for QBF. We evaluate the usage of QBF in bounded model checking (BMC), using general-purpose SAT and QBF solvers. We develop a special-purpose decision procedure for QBF used in BMC, and compare our technique with the methods using general-purpose SAT and QBF solvers on real-life industrial benchmarks.