...Website available for archives only...
...Not updated...

Computer Science

Probabilistic Abstract Interpretation (Paper, Talk, BibTeX)

This paper, written with P. Cousot, proposes a new formalism for static analysis of programs that involve probabilities. It extends classical abstract interpretation and allows for easy lifting of existing non-probabilistic analyses. It has been published at ESOP 2012.

The paper along with an extended version (with proofs and introduction) can be found below, also with the slides of the talks to give the intuitions behind the framework:

Predicting cache contents by abstract interpretation (Powerpoint)

Talk at NEVER seminar at NYU - joint work with Chris Hankin at Imperial College.

Description of a new framework to statically predict cache contents at runtime. This new abstrat domain is modular and allows for replacement strategies and hierarchies switching. It thus applies easily (and automatically) to every practical situations. (The more precise paper is currently being written.)


Abstract Interpretation, contracts and object invariants (Internship at Microsoft Research 2009, PDF, PDF)

This is the report for the internship I made at Microsoft Research in Redmond during Summer 2009. It is focused on a new technique to ensure that contracts can be persisted between analyses and on the implementation of object analyses in Clousot, the static analyzer for .NET languages developed by Microsoft Research.

Download, Téléchargement

Gadgets, approximability and the PCP theorem (2009, PDF)

This work was made for a workshop on the PCP theorem at the ENS. It mainly deals with gadgets and their generation for allowing optimal and automatic reductions between usual algorithmic problems (e.g. MaxCut). Then some results related to the PCP theorem are stated (but not always proved).


Pure functional programming : the use of monads (2009, PDF)

Monads, coming directly from category theory, are of great use in pure functional programming. This work explains how they can enable the programmer to use some impure paradigms in such a setting. Illustrated in Haskell.


Quantum computation : from exponential to polynomial (2008, PDF)

The goal of this study is to understand how quantum computation can make some algorithms exponentially faster, only with a small probability of error. We study Shor's and (briefly) Grover's algorithms.


Distorsion and graphs embeddings (2008, PDF)

This work was made with Arnaud de Mesmay.

It deals with some classical problems on graphs (Sparsest Cut and Multicommodity flow), which are known to be NP-complete. The goal is to approximate optimal solutions with a polynomial algorithm.

To accomplish that goal, we study some recent papers of Linial, London and Rabinovich where the main idea is to embed graphs into some .

PDF of the report & Program (see the PDF) - Windows required, uses OpenGL.

Kummer's cardinality theorem (2007, PDF)

We study here Kummer's cardinality theorem (1992): a spectacular result in decidability theory.

PDF of the report & Presentation





Transversality and genericity (2007, PDF)

The goal here is to understand René Thom's transversality theorem. It is a result in differential geometry which tries to quantify the fact that some situations are “very unlikely” (think of a matrix being singular for a trivial example). The theorem is then applied to Morse functions.

Download full version of my second TIPE - part of the French competitive examinations for CPGE.

Conjugacy of -endomorphisms (2006, PDF)

The topic is the study of linear dynamical systems, and the caracterisation of the situation where two hyperbolic systems are “equivalent”, ie. where their integral curves “behave the same”. These notions are of course formally and precisely expressed.

So we begin by classifying -endomorphisms, and we apply the results to prove the Großman-Hartman theorem.

Download full version of my first TIPE.