- A-212 (STCS Seminar Room)
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.