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
-
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 successfully 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 my masters degree from Sorbonne University, focused on the theory of programming languages, functional programming and formal methods (notably static analysis by abstract interpretation and theorem proving with the Rocq prover).
To reach out, you can write to me at hra687261(at)gmail(dot)com.
Professional experience
-
R&D Engineer at OCamlPro, since Sep 2021.
-
PhD Student at Université Paris-Saclay, CEA, List, from Sep 2022 to Oct 2025.
-
R&D Intern at OCamlPro, from Mar 2021 to Sep 2021.
Education
-
Doctorate in computer science from Paris-Saclay University, successfully defended on the 15th Oct 2025. More info at defense page.
-
Master's degree in computer science from Sorbonne University, Sep 2021.
-
Title: Software Science and Technology (Fr: STL — Science et Technologie du Logiciel), R&D branch, Software safety and reliability thematic. -- - Main subjects: Algorithmics, Formal methods, Type checking, Static analysis, Program verification, Operational semantics and Process algebras.
-
-
Bachelor's degree in computer science from Sorbonne University, Sep 2019.