About Me

My picture

I am a computer scientist specialized in code analysis to make software safer.

I took part in many projects that aims at soundly verifying source code using static analysis for critical software systems. In particular, I worked in collaboration with AbsInt GmbH and Airbus to improve analysis methods to prove safety and security of low-level software, such as OSes.

Learn more about my PhD thesis, my defense, and the minutes of the jury here.

I also have a strong background in math and extensive experience in big software development, making me able to tackle most challenges in software systems.

Education & Experience

2017-2020

PhD.

ENS (Antique team)

Proving the security of software-intensive embedded systems by abstract interpretation.

  • Mathematic Lectures (LFDV, CRI, Paris, FR)
    Lectures on logic, set theory, functions and linear algebra in 1 st year of Frontiers of Life Sciences Bachelor at CRI. 104h
  • Tutorial of Semantics Lecture (ENS, Paris, FR)
    Exercise and practical sessions + 2 lectures. 75h

2014-2016

M. Sc.

EPFL / ENS de Lyon

MS. in theoretical computer science obtained with highest honors (17.5/20).

2013-2014

B. Sc.

ENS de Lyon

B.Sc. in theoretical computer science obtained with honors (15.84/20)

  • Research internship (LIX, Alco team)
    Characterization of the functions calculated by a Turing machine with a bound on the number of transitions with a change of state

My Skills

I'm an expert in C++17. I also master OCaml, LATEX, Python and x86.

Furthermore, I have vast knowledge in theoretical computer science and mathematics, in particular, logic, semantics, computability theory, probability and algorithmics.


C++

Python

OCaml

Others


And even more

Projects

AstréeS Astrée logo

ENS, Antique team [2016 - 2020], OCaml

State of the art static analyzer based on abstract interpretation with industrial applications developped at Antique since 2001.


Socrates

[2019 - Present], Python

Advanced and generic testing tool motivated by Astrée.


OColor

[2019 - Present], OCaml

Pretty printing library using Format’s semantic tags to generate well-parenthisized ANSI escape sequences.


TuringSim

[2014 - Present], C++

Template-intensive high-performance framework for simulation of abstract computation model.


Platypus

ENSL, team of 7 people [September 2014 - Present]

A modular and open source question answering framework. Initially a team of seven students, now an open source project.

More information on the project website. You can also try the online demo.


Megasat

ENSL, team of 2 people [Feb. 2014 - May 2014], C++

SAT and SMT solver using state of the art algorithms


Introduction à la calculabilité (Introduction to computability theory)

[Oct. 2011 - Present]

Write a 300 pages paper introducing to compatibility theory


2021 Chevalier