Sciweavers

Share
SAT
2005
Springer

Bounded Model Checking with QBF

12 years 1 months ago
Bounded Model Checking with QBF
Current algorithms for bounded model checking (BMC) use SAT methods for checking satisfiability of Boolean formulas. These BMC methods suffer from a potential memory explosion problem. Methods based on the validity of Quantified Boolean Formulas (QBF) allow an exponentially more succinct representation of the checked formulas, but have not been widely used, because of the lack of an efficient decision procedure for QBF. We evaluate the usage of QBF in BMC, using general-purpose SAT and QBF solvers. We also present 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. Our procedure performs much better for BMC than the general-purpose QBF solvers, without incurring the space overhead of propositional SAT.
Nachum Dershowitz, Ziyad Hanna, Jacob Katz
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where SAT
Authors Nachum Dershowitz, Ziyad Hanna, Jacob Katz
Comments (0)
books