I'm a Senior Scientist at Inria, leading the Toccata research group, common to the Research center INRIA Saclay - Île-de-France and the Laboratoire de Recherche en Informatique. I'm member of the VALS group of LRI.
My research activities belong to the general topic of mechanized proof of properties of programs. This topic belongs to the so-called domain of Formal Methods for Software Engineering.
By mechanized proof I mean two possible things. In a first case, the proof can be fully automated, in the sense that a given property is given to a computer, and the computer must find a proof for it. In a second case, proof is done interactively: this can be done using some tactics proposed by the user to perform the proof, or more generally, in the context of program verification, extra annotations can be given: auxiliary lemmas, extra code assertions, invariants, etc. But in all cases, the proof is checked valid by a computer tool.
I always wanted my research activities to be substantiated by experimental validation. This is why I developed (or contributed to) several tools, described below, and I made the necessary efforts to make such tools not only prototypes but maintain them, distributed them, and provide some support to users.
Program Verification tools
- Why3: A multi-input multi-prover verification platform
- Why (version 2): the former version of Why (includes Krakatoa and the Jessie plug-in of Frama-C)
- Frama-C: Environment for Static Analysis of C source, developed in collaboration with CEA-List and now mainly maintained by CEA
- SPARK2014: Environment for the safe development of critical applications in Ada, developed by AdaCore. We contribute to the proof tool of SPARK2014, in the context of the ProofInUse common laboratory.
- Joint Laboratory ProofInUse with AdaCore (ANR, programme LabCom, 2014-2017)
- BWare: Framework for automated verification of B proof obligations (ANR, programme Ingénierie Numérique & Sécurité, 2012-2016)
- Hi-Lite, FUI project (2010-2013)
- COST european project: Verification of Object-Oriented Software (03/2008-02/2012)
- HISSEO Verification of Floating-Point Programs (Digiteo 09/2008-02/2012)
- U3CAT Unification of Critical C Codes Analysis Techniques (ANR Arpège 08, 01/2009-09/2012)
- Cepromi Certification de Programmes Manipulant la Mémoire (INRIA ARC, 01/2008-12/2009)
- CAT C Analysis Toolbox (ANR RNTL 01/2006-12/2008)
- GECCOO Génération de code certifié pour des applications orientées objet Spécification, raffinement, preuve et détection d'erreurs (ACI Sécurité, 07/2003-12/2006)
- VERIFICARD tool-assisted specification and verification of JavaCard programs (European IST project 01/2001-09/2003)