About me

My name in Anne Pacalet, and 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, you can now try part of our tools, like tis-interpreter, online to find undefined behaviors in your own programs.

Frama-C

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 :

  • a PDG (Program Dependence Graph) computation,
  • a spare code elimination function based on the PDG,
  • a slicing tool that proposes different selection modes and makes possible to tune the precision.
  • the Scope plug-in which uses other plug-ins results to highlight the code in the GUI in order to give semantic dependencies information to help browsing unknown programs or find bugs. See here an interesting use case.
  • I also started to write a verification condition generator based on WP computation which is now integrated as the WP plug-in. But some other people are working on it now.

CAVEAT

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 :

  • front-end compilation,
  • Weakest-Precondition computation,
  • rewriting techniques to simplify expressions,
  • precondition generation to detect run-times errors,
  • alias analysis,
  • abstract interpretation,
  • user interface (graphical or not),
  • and probably many other things…

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.

EasyCrypt

I also worked with Benjamin Gregoire in the Marelle team at Inria Sophia-Antipolis on the CertiCrypt projects. 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.

Others

Table des matières
Tags
Dernières notes