A Verified QBF Solver

Abstract: Quantified Boolean Formulas (QBFs) extend propositional logic with universal and existential quantification over Boolean variables.  A QBF is satisfiable if and only if there is an assignment of Boolean values to the free variables that makes the formula true, and a QBF solver is a software tool determining if a given QBF is satisfiable. This thesis introduces formalizations of, and correctness proofs for, two QBF solvers in the Isabelle/HOL interactive theorem prover.  One solver is based on naive quantifier expansion, while the other uses a search-based algorithm.  While experiments show that the verified solvers have performance far behind the state-of-the-art in QBF solving, they provide unparalleled confidence in correctness.  To our knowledge, these are the first QBF solvers to be formally verified using interactive theorem proving.