I'm a PhD student at the
BINSEC Team,
working from NanoINNOV at
CEA Paris-Saclay.
My PhD subject is centered around SSA translation by abstract interpretation.
I work under the supervision of
Matthieu Lemerre.
My research interests focus on verification and low-level systems:
formal methods, abstract interpretation, type systems, Coq, operating systems, compilers, hardware, functionnal programming and more.
Besides computer science, I also enjoy mathematics and physics.
I like to code in my free time. You can find my personal projects,
such as bibtex autocomplete
or my solutions for advent of code
on the software page.
My hobbies include outdoor sports such as rock climbing, sailing, hiking and skiing.
I also enjoy reading, especially sci-fi and detective stories.
You can also find me playing board games and video games
Dorian Lesbre
and Matthieu Lemerre
PLDI 2024
Abstract
Rewriting and static analyses are mutually beneficial techniques: program transformations change the inten-
sional aspects of the program, and can thus improve analysis precision, while some efficient transformations
are enabled by specific knowledge of some program invariants. Despite the strong interaction between these
techniques, they are usually considered distinct. In this paper, we demonstrate that we can turn abstract
interpreters into compilers, using a simple free algebra over the standard signature of abstract domains.
Functor domains correspond to compiler passes, for which soundness is translated to a proof of forward
simulation, and completeness to backward simulation. We achieve translation to SSA using an abstract do-
main with a non-standard SSA signature. Incorporating such an SSA translation to an abstract interpreter
improves its precision; in particular we show that an SSA-based non-relational domain is always more precise
than a standard non-relational domain for similar time and memory complexity. Moreover, such a domain
allows recovering from precision losses that occur when analyzing low-level machine code instead of source
code. These results help implement analyses or compilation passes where symbolic and semantic methods
simultaneously refine each other, and improves precision when compared to doing the passes in sequence.
Labeled Union-Find for Constraint Factorization
‐
Short paper
Matthieu Lemerre
and Dorian Lesbre
NSAD 2024
Abstract
In this work-in-progress paper, we present labeled union-find,
an extension of the union-find data structure where
edges are annotated with labels that form a group algebraic
structure. This structure allows to very efficiently represent
the transitive closure of many useful binary relations, such as
two-variables per equality (TVPE) constraints of the form
y = ax+b. We characterize the properties of labeled union-find
when used to represent binary relations between variables.
More specifically, we study the use of this domain in a static
analysis; either to represent binary relations, or as a reduced
product with non-relational abstract domains with constraint
propagation; as well as the design of efficient algorithms for
the join of labeled union-find structures. We believe that this
structure could be used as a low-cost relational domain or
decision procedure, and that it could make other relational
domains more efficient by removing the need to track some
variables.
In no particular order, here are a few links ranging from useful software
to some fun games and comics.
Software
- KeePassXC is a password manager. It allows you to use very secure passwords without fear of forgetting them.
- Obsidian is an note-taking app that is both simple (based on markdown files)
and very customizable thanks to a large plugin ecosystem.
- Typst is a interesting alternative to LaTeX which fixes a good chunk of what I find frustrating with TeX.
- Godbolt website that can compile small programs and show generated assembly. I find
the ability to show assembly diff between two similar programs very helpful. It allows to quickly
see how small changes affect the generated code.
- Syncthing is a great, privacy respecting file synchronisation tool.
- Sioyek is a PDF reader well suited to reading scientific papers.
- Connected papers website displaying links between scientific publications as a graph. Very handy for bibliographic exploration.
Webcomics
- XKCD a webcomic about physics, science and other stuff
- Garfield a webcomic about an adorable fat orange cat
Video games
- Kerbal Space Program a game for space and physics fans! It allows you to design and launch your own rockets.
- Outer Wilds an exploration game set in a miniature solar system, this gem will take you on a memorable journey.
- Return of the Obra Dinn short detective game which trusts players to find well hidden clues and make complex deductions
- Factorio behind some unattractive graphics, factorio hides a very engaging and satisfying game about optimisation and logistics
