Je suis étudiant en doctorat à
l'équipe BINSEC,
au centre NanoINNOV du
CEA Paris-Saclay.
Je travaille sur l'interprétation abstraite par transformation SSA. Mon encadrant
de thèse est Matthieu Lemerre.
Je m'intéresse notamment à la vérification et l'informatique pratique bas niveau :
méthodes formelles, interprétation abstraite, système de types, Coq, systèmes d'exploitation, compilation,
circuits, programmation fonctionnelle et d'autres. En dehors de l'informatique, je m'intéresse
aussi aux mathématiques et à la physique.
J'aime aussi programmer dans mon temps libre, vous trouverez sur la page
logiciels mes projets
personnels comme bibtex autocomplete
ou mes solution de l'advent of code .
Hors du domaine scolaire, j'aime bien faire des sports d'extérieur comme l'escalade, la voile, la randonnée
et le ski. J'aime bien lire, notamment de la SF et des romans policiers. Je m'occupe également en jouant à des jeux de société et des jeux vidéos.
Dorian Lesbre
et Matthieu Lemerre
PLDI 2024
Resumé
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
‐
Papier court
Matthieu Lemerre
et Dorian Lesbre
NSAD 2024
Resumé
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.
Sans ordre particulier, voici quelques liens allant d'outils que
j'utilise régulièrement pour le travail, à des comics et jeux que
j'apprécie beaucoup.
Logiciels
- KeePassXC (en) est un gestionnaire de mot de passe, il permet d'utiliser des mots de passe sécurisés sans risque d'oubli.
- Obsidian (en) est une application de prise de notes simple (à base de fichiers markdown)
et très riche grâce à un bel écosystème de greffons.
- Typst (en) est une alternative a LaTeX assez complète qui adresse bon nombre de mes frustration avec TeX.
- Godbolt (en) site web permettant de compiler des petits programmes et d'afficher l'assembleur généré.
Je trouve la visualisation de diff de codes particulièrement utiles pour voir l'effet d'un petit changement
dans la source sur le code généré.
- Syncthing (en) est un très bon outil de synchronisation de fichiers entre plusieurs appareils.
- Sioyek (en) est un lecteur de PDF très adapté à la lecture de publications scientifiques.
- Connected papers (en) site web affichant les citations entre publications scientifiques sous forme de graphe. Très pratique pour l'exploration bibliographique
Webcomics
- XKCD (en) un webcomic sur la physique, la science et plein d'autre choses
- Garfield (en) un webcomic au sujet d'un (adorable) gros chat orange
Jeux vidéos
- Kerbal Space Program un jeu pour les fans de physique et d'espace ! Il permet de concevoir et lancer ses propres fusées.
- Outer Wilds Un jeu d'exploration et de découverte dans un système solaire miniature, il vous embarquera pour un voyage inoubliable.
- Return of the Obra Dinn court jeu de détective qui fait confiance au joueur pour trouver des indices bien dissimulés et faire des déductions difficiles.
- Factorio derrière ses graphismes peu attirants, factorio cache un jeu d'optimisation et de logistique très prenant et satisfaisant.
