William Klieber

Formal Verification Using Quantified Boolean Formulas (QBF) Degree Type: Ph.D. in Computer Science
Advisor(s): Ed Clarke
Graduated: May 2014

Abstract:

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 prenex conjunctive normal form (CNF). However, the Tseitin transformation (which is used to convert a formula to CNF) is asymmetric between the two quantifier types. In particular, it introduces new existentially quantified variables, but not universally quantified variables. It turns out that this makes it harder for QBF solvers to detect when a formula has become true (but not when a formula has become false) under an assignment.

We present a technique using ghost variables that handles non-CNF QBF formulas using a symmetric alternative to the Tseitin transformation. We introduce sequent learning, a reformulation and generalization of clause/cube learning. With sequent learning, we can handle non-prenex formulas. Whereas clause/cube learning only allows learning when the whole input formula becomes true or false, sequent learning allows us to learn when a quantified subformula becomes true or false.

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 ∃x: (x ∧ y) ∨ z is the formula y ∨ z.

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.

Thesis Committee:
Edmund M. Clarke (Chair)
Randal E. Bryant
Jeannette M. Wing
João P. Marques-Silva (University College Dublin)

Frank Pfenning, Head, Computer Science Department
Randy Bryant, Dean, School of Computer Science

Keywords:
Formal verification, formal methods, model checking, QBF, SAT, non-prenex, non-clausal, DPLL, CEGAR