Formally Certified Satisfiability Solving

Abstract

Satisfiability (SAT) and satisfiability module theories (SMT) solvers are efficient automated theorem provers widely used in several fields such as formal verification and artificial intelligence. Although SAT/SMT are traditional propositional and predicate logics and well understood, SAT/SMT solvers are complex software highly optimized for performance. Because SAT/SMT solvers are commonly used as the final verdict for formal verification problems, their correctness is an important issue. This talk discusses two methods to formally certify SAT/SMT solvers. First method is generating proofs from solvers and certifying those proofs. One of the issues for proof checking is that SMT logics are constantly growing, therefore a flexible framework to express proof rules is needed. The proposal is to use a meta-language called LFSC, which is based on Edinburgh Logical Frame with an extension for expressing computational side conditions. SAT and SMT logics can be encoded in LFSC, and the encoding can be easily and safely extended for new logics. And it has been shown that an optimized LFSC checker can certify SMT proofs very efficiently. Second method is using a verified programming language to implement a SAT solver and verify the code statically. Guru is a pure functional programming language with support for dependent types and theorem proving. A modern SAT solver has been implemented and verified to be correct in Guru with low-level optimizations. Also, Guru allows very efficient code generation through resource types,so the performance of versat is comparable with that of the current proof checking technology.

Short bio

Resources

• talk slide