Je suis Directeur de Recherche à l'Inria, responsable de l'équipe de recherche Toccata , commune au centre de Recherche INRIA Saclay - Île-de-France et du Laboratoire Méthodes Formelles.
Activités de recherche
Mes activités de recherche appartiennent à la thématique générale de la preuve mécanisée de propriétés de programmes. Cette thématique fait partie du domaine des méthodes formelles pour le développement logiciel.
Par preuve mécanisée je veux exprimer deux choses possibles. Dans un premier cas, la preuve peut être entièrement automatisée, dans le sens où une propriété est exprimée formellement, et l'ordinateur doit en trouver une preuve. Dans un deuxième cas, la preuve est faite de manière interactive: par exemple en utilisant des tactiques proposées par l'utilisateur pour effectuer la preuve, ou plus généralement, dans le cadre de la vérification de programme, des annotations supplémentaires peuvent être données: lemmes auxiliaires, code supplémentaire, assertions, invariants, etc. Mais dans tous les cas, la preuve est validée formellement par un outil informatique.
Voir le rapport d'activité annuel de l'équipe Toccata (en anglais) pour plus de détails sur mes activités autour de la vérification de programmes. J'ai aussi une certaine expérience spécifique de vérification de programmes numériques en virgule flottante.
J'ai toujours voulu que mes activités de recherche soient étayées par des validations expérimentales. C'est pourquoi j'ai développé (ou contribué à) plusieurs outils, décrits ci-dessous, et j'ai fait les efforts nécessaires pour que ces outils ne soient pas seulement des prototypes, pour les maintenir, les distribuer, et fournir du support aux utilisateurs.
Logiciels
Outils de vérification
- 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.
Autres
- bibtex2html: generation of HTML pages from bibliographies
Enseignement
Projets et contrats
Projets en cours
- 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.
Anciens projets
- Laboratoire Commun 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)