My doctoral work has been concerned with the certification of results of static analyses. Our approach is divided in two phases. First the reduction of our problem to the validity of verification conditions [Cor12, BCJd12], then the certification of the automatic proof of these conditions [BCP11a, BCP11b, BCS12].

Static Analysis Result Certification

The reduction of static analysis result certification to validity of verification conditions has been illustrated by a proof of concept developed in Why3 and Coq. The Why3 weakest precondition calculus is used as a VCgen-gen in the sense that given an operational semantics of the language and a concretisation function of the analysis, it produces the required verification conditions automatically. This work has been presented to the second Boogie workshop [Cor12], a satellite event of the CAV 2012 conference.

Unfortunately, even state-of-the-art solvers need careful parametrisation to discharge large VCs, and the result certification of complicated analyses may overwhelm solvers. To alleviate performance issues, we propose a reduction of generic VCs to less powerful VCs, tailored to a specific family of object-oriented analyses, including JAVA bytecode verification and null-pointer analyses [BCJd12].

SMT solver Result Certification

The certification of Satisfiability Modulo Theory solvers' results is necessary to maintain a controllable Trusted Computing Base in our case, but has many more applications. Apart from building trust in any application based on SMT solvers (and there are many of them in verification alone), developing a result checker with a mechanised proof for these tools paves the way to integration of SMT solvers in proof assistants, in our case: Coq.

We developed a Nelson-Oppen proof system together with a checker programmed in Coq [BCP11a] based on specific proofs systems. To change an existing theory or add a new theory to the certified decision procedure, our checker needs only an implementation of a checker for the new theory and its proof. This work has been presented at the first CPP conference [BCP11b], including experimentation with a combination of arithmetic and Equality and Uninterpreted Functions theory, and the dedicated proof-systems for these theories. A comparison of checkers for the EUF theory has been presented at the second PxTP workshop [BCS12], a satellite event of the IJCAR 2012 conference.

DeCert project

I had the opportunity to collaborate to the ANR project Decert, on the certification of decision procedures. One of the task of the group was the integration in Coq of SMT solvers. Our approach to SMT solver result certification was part of this work, and gave us the opportunity to collaborate with other members of the consortium. I take advantage of this web page to link the website of the project where more (relevant) information can be found.

ASCERT project

My PhD studies are funded by the ASCERT project.

Master thesis

I had a 5 months research internship in the Celtique team, supervised by Frédéric Besson, dealing with the certification of combinations of decision procedures. That work is based on the Nelson-Oppen algorithm, and try to introduce a general framework to combine different certificate formats, for different logics, in a global format certifying mixed logics. Subsequently we propose a certificate format for the theory of equality with uninterpreted functions.

report : Vérification efficace de preuves de programmes [.pdf]

That internship led to my master thesis, defended in September 2009, leading to my MPRI diploma (Computer Science Research Master of Paris), obtained with distinction.