Ph.D. Oral Proposal: Nathan Wetzler, GDC 7.808

Contact Name: 
Lydia Griffith
Oct 18, 2013 10:00am - 12:00pm

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


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