Formal proof producing decision procedures

December 3, 2009
Assia Mahboubi | French National Institute for Research in Computer Science and Control (INRIA).

Automated decision procedures nowadays play a crucial role in the verification process of real life code. The breakthrough introduced by SAT and then SMT solvers make them very widely use to help developers prove assertions about the correctness of their code. Yet these tools, especially in the case of SMT solvers, often give little explanation about their answer, which can become an obstacle when certifying critical code. In this talk I will describe how formal proof assistants can help in that case, which approaches are already available for this task, and the challenges this problem raises for proof assistants.

Speaker Details

Assia is a permanent full-time researcher at the French National Institute for Research in Computer Science and Control (INRIA). She also works in Georges Gonthier’s group Mathematical Components at the Microsoft Research INRIA Joint Centre. This group works on designing modular, reusable libraries of formalized mathematics. Its objective is to demonstrate the success of these methods by providing a formal proof of a famous result in finite group theory, the so-called Feit-Thompson Theorem.She is also working on proof producing decision procedures for the Coq proof assistant. During her PhD, she implemented a Cylindrical Algebraic Decomposition (CAD) algorithm in the Coq system in order to provide a complete decision procedure for non-linear real arithmetic, and an efficient proof producing decision procedure for the equational theory of rings and semi-rings. She is now interested in specialized decision procedures crafted for the verification of SMT traces.