Bio

PhD, R&D engineer at OCamlPro, my work and research interests lie in the field of formal methods and their applications. I am notably interested in SMT solving, Symbolic Execution, Deductive Verification and Constraint Programming. Check out my publications page to see some of my work.

Among the projects I work on/contribute to:

• Alt-Ergo: An SMT solver, designed for program verification. Source

• Colibri2: A CP solver for SMT problems. Source

• Owi: A symbolic execution engine for Wasm programs. Source

• Smtml: An OCaml library offering a common front-end for multiple SMT solvers. Source

• Dolmen: A library and tool that offers, parsing, type-checking and model verification for SMT-LIB problems (and problems in other logic languages). Source

In 2025, I succesfully defended my PhD thesis titled "A theory of sequences tailored for program verification", which I prepared jointly at OCamlPro and the CEA-List lab of University Paris-Saclay. In 2021, I obtained a masters degree from Sorbonne University, focused on the theory of programming languages, functional programming and formal methods (notably abstract interpretation and theorem proving with Rocq). See my CV page for a full overview of my background.

To reach out, you can write to me at hra687261(at)gmail(dot)com, or through the links below.