I am a third year PhD student in Computer Science at ENS Paris and Inria Paris in Antique team under the direction of Jérôme Feret. My field of research is formal methods and their usage for static analysis of programs, in particular by abstract interpretation.
I am passionate about understanding what truly happens under the hood of programs and systems. I am particularly interested in formal methods and the mathematical foundations of programming, which enable writing software that is not only safer but also clearer and more robust.
At the same time, I am drawn to the intricacies of real-world systems — such as designing or analyzing the semantics of a CPU — and I value the challenge of bringing formal rigor to complex, practical settings.
I am proficient in programming languages and tools such as
I also have some knowledge of other languages and tools such as
This work contributes to the static analyzer Astrée — specifically its security-focused version, AstréeS — to analyze the safety of embedded critical systems with significant software components. My focus is on analyzing operating systems that make use of paged memory.
For three consecutive years, I was responsible for leading the tutorial sessions of the Programming Languages and Compilation course taught by Jean-Christophe Filliâtre to third-year undergraduate students at ENS. In particular, I assisted students with their projects involving the development of compilers for subsets of the following three languages: C with support for nested functions, PureScript with partial support for type classes, and Koka with partial support for effects.
I have been co-managing the weekly Antique's team seminar — the SémAntique — with Bernadette Charron-Bost for 3 years.
Member of the Server team within the internal tooling unit during the first half of the internship: I contributed to the maintenance and development of the API and various internal tools used by the support, data , and sales teams, among others.
In the second half, I worked on a research and development project exploring the use of post-quantum cryptography for data sharing in Dashlane. As part of this, I created bindings for the implementations of the NIST competition finalists into code executable in the browser, along with a playground to compare the algorithms.
I also contributed — as part of a hackathon in the first place — to the development of the Dashlane's command-line interface.
Master's project involving the addition of an abstract interpretation phase to Stainless, a static analysis tool for Scala programs. This enhancement enables the automatic computation of loop invariants, reducing the amount of user input required to verify program properties.
Internship advised by Eddy Caron about the bootstrapping of the SkyData project, exploring decentralized data management through distributed algorithms and autonomous agent-based systems.
Internship co-supervised by Marc Chevalier and Jérôme Feret about the formalization and implementation of static analysis by abstract interpretation of inline assembly in C code.