Talks & Seminars
Title: Faculty Candidate Talk - Ashish Darbari SHRUTI: An Industrial Strength Formally Certified SAT Solver.
Dr. Ashish Darbari, University of Southampton in England.
Date & Time: October 28, 2009 11:00
Venue: KReSIT Conference Room
HRUTI: An Industrial Strength Formally Certified SAT Solver 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 core of the system is a certified checker for unsatisfiable claims that is formally designed and implemented in Coq. I will present the design and correctness aspects in the talk, and show some 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.5x) than the uncertified solvers PicoSAT/Tracecheck and zChaff/ZVerify; it is faster (32x) than the previously developed certified checkers implemented on top of other LCF-style theorem provers such as HOL4 and Isabelle. ______________________________________________________________________
Speaker Profile:
Dr. Ashish Darbari works as a Post-Doc Research Fellow at the University of Southampton in England.
List of Talks


Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback