About Me

My picture

I am a specialist in Computer Science highly skilled in developping reliable critical software.

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.

In particular, I took part in many projects that aims at soundly verifying source code using static analysis for critical software systems, especially using abstract interpretation.

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

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