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 Méthodes Formelles.
Research Activities
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.
See the Annual research report of the Toccata group for more details on my activities around program verification. I also have some specific experience in the verification of floating-point programs.
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.
Software
Program Verification tools
- Why3: A multi-input multi-prover verification platform
- 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.
Other Software
- bibtex2html: generation of HTML pages from bibliographies
Teaching
Projects, Contracts and Grants
Ongoing projects
- As part of the ProofInUse Consortium:
- Bilateral contract with TrustInSoft company (2020-2024)
- Bilateral contract with Mitsubishi Electric R&D Centre-Europe (2019-2024)
- Bilateral contract with AdaCore company (2019-2023)
- Project Décysif: Formal Verification for Safety and Security, co-funded by French government and Ile-de-France region, under the i-Demo call of plan de relance France 2030.
Past projects
- Joint Laboratory ProofInUse with AdaCore (ANR, programme LabCom, 2014-2017)
- CoLiS: Correction of Linux Scripts (ANR, 2015-2019)
- 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)