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.

I am a PhD student at The University of Iowa and a member of the Computational Logic Center, led by Prof. Cesare Tinelli and Prof. Aaron Stump. My research area is satisfiability modulo theories, formal verification and dependent type systems. I'm interested in verifying functional properties of real-world software systems using formal methods.