Contact Version française

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.


Program Verification tools

Other Software


Projects, Contracts and Grants

Ongoing projects

Past projects