Anne Pacalet

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, ...

Some time ago, I spent most of my time implementing known analyses, but I often had to adapt them to fit the real word, because the C language is somehow different from the ideal language often used in academic papers. I also tried to develop new ideas, from time to time, and I even tried to formalize some of them using the proof assistant COQ.

In 2012-2013, I have been working for SafeRiver where my work was rather to study how some formal tools could be used on real world customer programs, and also how to adapt them to better fit industrial needs.

Now, from Decembrer 2013, I work for TrustInSoft where I try to contribute to deliver guaranties on the absence of the most common security flaws in software. If you are interested, tis-interpreter is now available on GitHub so you can try it on your own programs to find undefined behaviors!


Frama-C is a platform 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 I personnaly worked on different subjects like :

Certificate Translator

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. A paper presenting it has been accepted at ICFEM 2009.


I also worked with Benjamin Gregoire in the Marelle team at Inria Sophia-Antipolis on the CertiCrypt project. I was in charge of the implementation of the first prototype version of the Easycrypt tool which is an automated tool for elaborating security proofs of cryptographic systems from proof sketches.


E-mail: Anne dot Pacalet at free dot fr

Valid XHTML 1.0 Strict Valid CSS! logo Vim