Current research

Proof carrying code. We have applied my Phd work on Proof Carrying Code (or more precisely certificate checker certification). We propose an abstract interpretation framework to build PCC architecture with a downloadable Coq soundness proof of the certificate checker. The architecture has been evaluated experimentally on a byte code language for which we have designed an interval analysis that allows to generate certificates ascertaining that no array-out-of-bounds accesses will occur (see our TCS'06 paper for more details).
We are currently extending this work with polyhedral analysis techniques in order to compute resource bounds on Java programs.

Information flow type systems We have implemented and proved correct in Coq a modular type checker for Java bytecode programs. This work has been presented at ESOP'07. This works was mainly achieved during my postoc in the Everest team at INRIA Sophia-Antipolis.

Certified static analysis. My phd's works dealt with the development of certified static analyses using the Coq proof assistant and the abstract interpretation theory. This PhD was done under the direction of David Cachera and Thomas Jensen. It takes place at Irisa in project Lande during september 2002 and september 2005. During this work, I have developed static analyses for a programming language similar to Java bytecode. The extraction features of Coq have enabled me to extract an analyser written in OCaml, from the correctness proof of the analysis. The correctness proof follows the abstract interpretation methodology. The main theorem establishes that the analyser computes correct informations with respect to the operational semantics of a program. I propose a generic framework to formalise static analysers in Coq. This work is mainly explained in a TCS'05 article.

Formal Java Bytecode semantics. I participate to the the development of Bicolano, a Formal Java Bytecode semantics written in Coq for the Mobius european project.

Software development

Past research

General recursion in Coq. We have worked on an extension of Coq to facilitate the definition and the reasoning of recursive general functions. This work has led to a paper in FLOPS'06.

Various Coq formalisations. My previous research activities were related to formalisation in Coq of geometrical algorithms like computation of convex hulls (see TPHOLs' 01 paper), proof of programs describing hardware implementations using systems of affine recurrence equations (see TPHOLs' 03 paper) and formalisation, in PVS, of an algorithm of optimization used for the compilation of JavaCard programs (see COCV' 03 paper).