Boolean satisfiability (SAT) solvers are not only routinely used in the formal verification of large industrial problems, but also applied in safety-critical domains such as the railways, avionics, and automotive industries. However, the use of SAT solvers in such domains requires some form of assurance for the results, as the solvers can have bugs. The complexity of modern, highly optimized SAT solvers makes it very difficult to provide a formal proof of correctness.
In this talk I will present a new approach for certifying SAT solvers where an un-trusted, industrial-strength, SAT solver is plugged into a trusted, formally certified, SAT proof checker to provide an industrial-strength formally certified SAT solver --- SHRUTI. The three key novelties of our approach are:
1. Our checker is formally designed and proven correct in an LCF style proof assistant and is automatically extracted from the proof assistant.
2. It is used as a standalone executable program independent of any supporting theorem prover, and
3. It certifies any SAT solver respecting the agreed format for satisfiable and unsatisfiable claims.
The main part of our work involves implementing a certified proof checker for unsatisfiable claims that is formally designed, verified, and implemented inside Coq. I will present its design and outline the correctness aspects in the talk, and show evaluation results of SHRUTI on a representative set of industrial benchmarks from the SAT Race Competition. The performance results demonstrate that whilst SHRUTI is slower (~2.5 times) than the uncertified solvers PicoSAT/Tracecheck and zChaff/ZVerify it is faster (upto 32 times) than the previously developed certified checker implemented on top of the HOL 4 theorem prover.
