CMU-CS-14-117Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-14-117
William Klieber May 2014 Ph.D. Thesis
Keywords:
Formal verification, formal methods, model checking, QBF, SAT,
non-prenex, non-clausal, DPLL, CEGAR
Many problems in formal verification of digital hardware circuits and other finite-state systems are naturally expressed in the language of quantified boolean formulas (QBF). This thesis presents advancements in techniques for QBF solvers that enable verification of larger and more complex systems.
Most of the existing work on QBF solvers has required that formulas
be converted into
We present a technique using
Almost all QBF research so far has focused on closed formulas, i.e.,
formulas without any free variables. Closed QBF formulas evaluate to
either true or false. Sequent learning lets us extend existing QBF techniques
to handle open formulas, which contain free variables. A solution
to an open QBF formula is a quantifier-free formula that is logically
equivalent to the original formula. For example, a solution to the open
QBF formula ∃ The final part of this thesis discusses an approach to QBF that uses Counterexample-Guided Abstraction Refinement (CEGAR) to partially expand quantifier blocks. The approach recursively solves QBF instances with multiple quantifier alternations. Experimental results show that the recursive CEGAR-based approach outperforms existing types of solvers on many publicly-available benchmark families. In addition, we present a method of combining the CEGAR technique with a DPLL-based solver and show that it improves the DPLL solver on many benchmarks. 106 pages
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |