My main and favorite work is to try to build tools to help users to formally prove properties on their programs, more specifically C programs. I also worked on other static analyses of programs such as abstract interpretation, slicing, ...
I spend most of my time implementing known analyses, but I often have to adapt them to fit the real word, because the C language is somehow different from the ideal language often used in papers. I also try to develop new ideas, from time to time, and I have been trying to formalize some of them using the proof assistant COQ lately.
Frama-C is a quite new tool that can been seen as an evolution of Caveat (see below), but it doesn't share any code with its ancestor (one main reason is that Frama-C is developed in ocaml while Caveat was in C/C++). Moreover, Frama-C is designed to be an extensible platform, so it is quite easy to use it to test new ideas on C program analysis. Last but not least, Frama-C is Open Source software, so anybody can write his own plugins based on the results already computed by other analyzers.
I developed some plugins like :
I have been working for many years at CEA, in the Software Reliability Labs, where I developed some parts of Caveat : a static analysis tool for critical C programs.
We were quite happy that our tool had been used by Airbus to verify part of the embedded software of the A380 plane.
I learned a lot of things in this project and worked on different subjects like :
I worked a while in the Everest project at INRIA Sophia-Antipolis where I developed with Benjamin Gregoire a prototype of a proof transforming compiler for the Mobius project on Proof Carrying Code. It is available here, and a paper presenting it has been accepted at ICFEM 2009.
I wrote some small tools that are listed here.
Because I am quite old, I used to collect links on static analysis, programing languages and tools, Coq, and some others. Of course, now Google is my friend... but still...
I also keep some tips that might be usefull.