Ph.D. Oral Proposal: Nathan Wetzler Date: Friday, October 18, 2013 Time: 10:00am to 12:00pm Place: GDC 7.808 Supervisors: Warren Hunt, Jr. and Marijn Heule Title: Mechanically-Verified Validation of Satisfiability Solvers Abstract: Satisfiability (SAT) solvers are commonly used for a variety of applications, including model checking, equivalence checking, hardware verification, software verification, and debugging. These applications rely on the efficiency of SAT solvers to solve large problems and to provide the correct results. Solvers are often used not only to find a solution for a Boolean formula, but also to make the claim that no solution exists. In most applications, the absence of a solution represents the absence of errors. When no solution is reported to exist, we want to be confident that a SAT solver has fully exhausted the search space. This is complicated by the fact that state-of-the-art solvers employ a large array of complex techniques that are used to maximize efficiency. Errors may be introduced at a conceptual level as well as an implementation level. Formal verification is one approach to detect errors or to assure that the results produced by SAT solvers are correct. For my Ph.D. research, I propose the development of a fast, mechanically-verified satisfiability proof checker. Our approach has three major components: designing a suitable proof format, crafting an efficient proof checker, and mechanically proving the correctness of that proof checker. A successful project will yield a verified SAT proof-checking implementation that can validate proofs of unsatisfiability in a time competitive with, or ideally better than, the SAT solver that produced the proofs. We will demonstrate our approach by modifying state-of-the-art SAT solvers to emit proofs of unsatisfiability for a given formula that can then be used to derive a theorem of unsatisfiability in a theorem proving system, namely ACL2. Our proof checker is independent of the choice of satisfiability solver in order to accommodate ongoing developments in SAT solving technology.