SHF: Small: Mechanical Verification of QBF Results

University Of Texas At Austin, Austin TX

Investigators

Abstract

Many important industrial applications, such as verification and synthesis problems, can be efficiently solved by satisfiability (SAT) solvers. However, this approach involves translating the original problem into SAT that typically results in generating dozens to thousands of nearly identical copies of subproblems. The quantified Boolean formula (QBF) formalism provides a convenient framework to compactly translate many of these interesting problems. For example, software verification and hardware synthesis problems can be translated into QBF, while avoiding generating these nearly identical copies. Hence, QBF facilities a compact representation of crucial problems in computer science. The expressiveness of QBF comes at a price: it is hard validate the results produced by these solvers. The existing approaches for addressing this problem all have disadvantages. Prevalent approaches involve costly validation algorithms and limit the used techniques. A recent technological advancement, known as clausal proofs, takes care of most problems. However, efficiently checking clausal proofs is complicated, thus trusting the results of one complex program (a QBF solver) depends on the correctness of another complex program (the checker). To boost confidence in the results of QBF solvers, a mechanically-verified checker is required. This research develops a uniform, complete, and trustworthy framework for QBF solving which is urgently needed for the scientific and industrial application of QBF solvers.