I am a Software Engineer at Meta, within the WhatsApp dev infra Code analysis subteam. I mainly focus on static analysis of Erlang code to ensure reliability and safety properties of the WhatsApp server. In particular, I'm contributing to the open source Infer static analyser that we use at a large scale to prevent bugs in our applications.
Previously, I have worked for two years at MathWorks on the Polyspace static code analyser. I was part of the kernel development team: they leverage static analysis theories and technologies, in particular abstract interpretation, to formally prove the correction of critical software.
Before that, I was a PhD Student in the Antique team at the École Normale Supérieure in Paris, under the supervision of Antoine Miné. I also spent time in the APR team of Sorbonne Université. My topic was Abstract interpretation under weakly consistent memory models. I successfully defended on 26 February 2019. See my manuscript and defense slides (both in French).
Scientific interests
My main interest is the use of formal methods to ensure the security, safety and correctness of programs. I am particularly interested in static analysis by the means of abstract interpretation to automatically and soundly certify code properties such as the absence of some classes of errors.
I am also occasionnally interested in strong and expressive type systems and programming languages that use them, programming language implementation, and binary code analysis.
Publications
-
InfERL: scalable and extensible Erlang static analysis.
Ákos Hajdu, Matteo Marescotti, Thibault Suzanne, Ke Mao, Radu Grigore, Per Gustafsson, Dino Distefano. APLAS 2018.
Abstract. In this paper we introduce InfERL, an open source, scalable, and extensible static analyzer for Erlang, based on Meta’s Infer tool. InfERL has been developed at WhatsApp and it is deployed to regularly scan WhatsApp server’s Erlang code- base, detecting reliability issues and checking user-defined properties. The paper describes the Erlang specific technical challenges we had to address and our design choices. We also report on our experience in running InfERL on Erlang code at scale, supporting the messaging app used everyday by over 2 billion people.
-
Relational Thread-Modular Abstract Interpretation Under Relaxed Memory Models.
Thibault Suzanne and Antoine Miné. APLAS 2018.
Abstract. We address the verification problem of numeric properties in many-threaded concurrent programs under weakly consistent memory models, especially TSO. We build on previous work that proposed an abstract interpretation method to analyse these programs with relational domains. This method was not sufficient to analyse more than two threads in a decent time. Our contribution here is to rely on a rely-guarantee framework with automatic inference of thread interferences to design an analysis with a thread-modular approach and describe relational abstractions of both thread states and interferences. We show how to adapt the usual computing procedure of interferences to the additional issues raised by weakly consistent memories. We demonstrate the precision and the performance of our method on a few examples, operating a prototype analyser that verifies safety properties like mutual exclusion. We discuss how weak memory models affect the scalability results compared to a sequentially consistent environment.
-
From Array Domains to Abstract Interpretation under Store-Buffer-Based Memory Models.
Thibault Suzanne and Antoine Miné. SAS 2016.
Abstract. We address the problem of verifying concurrent programs under store-buffer-based weakly consistent memory models, such as TSO or PSO. Using the abstract interpretation framework, we adapt existing domains for arrays to model store buffers and obtain a sound abstraction of program states (including the case of programs with infinite state space) parameterised by a numerical domain. Whereas the usual method for this kind of programs implements a program transformation to come back to an analysis under a sequentially consistent model, the novelty of our work consists in applying abstract interpretation directly on the source program, setting a clean foundation for special dedicated domains keeping information difficult to express with program transformations. We demonstrate the precision of this method on a few examples, targetting the TSO model and incidentally being also sound for PSO due to some specific abstraction choice. We discuss an application to fence removal and show that our implementation is usually able to remove as many or more fences, with respect to the state of the art, on concurrent algorithms designed for sequential consistency while still remaining precise enough to verify them.
Programming
Here is some selected software I maintain or contributed to.
- Cormoran
-
An experimental static analyser for concurrent programs within relaxed memory models.
- Sterne
-
A scuba diving planner. Implements multi-gas staged decompression planification, air consumption and some other relevant tools. Includes a CLI interface and a mobile app.
- OCamlHamt
-
A Hash Array Mapped Trie library I implemented for OCaml during my internship in the Gallium Inria team. I also wrote a blog entry about it.
- OCamlgraph
-
A graph library for OCaml. I implemented the WeakTopological and ChaoticIteration modules for fixpoint computation using widening.
- HEVEA
-
A LaTeX to HTML translator. During my internship in the Gallium team, I reworked the output module with ropes and authored the HTML5 generator.
Teaching
I have been a teaching assistant in the following courses.
- 2017–2018
-
- Modèles de Programmation et Interopérabilité entre les Langages, L3. Sorbonne Université.
- Encadrement de projet STL (Sciences et Technologies du Logiciel), M1. Sorbonne Université.
- 2016–2017
-
- Introduction à la Programmation, L1. Université Paris Diderot.
- Langages et Automates, L2. Université Paris Diderot.
- 2015–2016
-
- Éléments d'Algorithmique, L2. Université Paris Diderot.
- Introduction à la Programmation, L1 CPEI. Université Paris Diderot.
- 2014–2015
-
- Introduction à la Programmation, L1. Université Paris Diderot.
Contact
Feel free to send me an email to my personal address .
