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 de Recherche en Informatique. I'm member of the VALS group of LRI.

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 Toccata web page for more details on the 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

Other Software

Teaching

Projects, Contracts and Grants

Ongoing projects

Past projects

Publications