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.
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)
- 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)