Contact English version

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 de Recherche en Informatique. Je suis membre de l'équipe VALS du LRI.

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 la page de l'équipe Toccata pour plus de détails sur les activités autour de la vérification du programme. 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

Autres

Enseignement

Projets et contrats

Projets en cours

Anciens projets

Publications