I work at Aesthetic Integration in Austin, Texas, on
Imandra, where I help
write a user friendly, powerful proof system based
on computational logic. I moved to Austin, Texas in January 2018.
Previously (2015-10 to 2017-10) I was at Inria Nancy doing a postdoc
with Jasmin Blanchette
on a counter-example finder for higher order logic,
I completed my PhD after 3 years at
from October 2012 to September 2015,
under the supervision of
Gilles Dowek and
My work takes place in the field of first-order automated
My thesis is titled
"Extending Superposition with Integer Arithmetic,
Structural Induction, and Beyond" and can be found below.
Before the PhD, I was a student in
École polytechnique, in France,
where I obtained an engineering diploma in 2012,
EPFL, in Switzerland, where I got a master
degree in Computer Science.
I am interested in Artificial Intelligence, formal logic, programming
languages; swing dancing with the Austin Swing Syndicate
(I'm applying for the board!);
classical music and opéra, science-fiction and more generally
I used to be a member of the
an association in charge of the students' network in École polytechnique.
Research engineer at Veridis with
Jasmin Blanchette, on model finding for higher-order logic.
PhD thesis at Deducteam
with Gilles Dowek and Guillaume Burel, on the topic of automated
A 3 months and a half internship at the ProVal lab in INRIA. The topic was about integrating TPTP provers in the Why software.
I'm interested in the technology of SAT solvers. More about it on
SAT. I'm also interested in first-order automated theorem
provers (in particular the technology of superposition, e.g.
the provers E and SPASS). I develop my own superposition prover, zipperposition, as a research test bed.
I converted the so called "Pelletier problems" (some small logical problems designed to test automated provers) in the TPTP format. The result is now in Zipperposition. The problem 28 is mistranslated (it seems to be satisfiable), although I could not find why. The last problems are not all translated.
Publications and documents
My dblp page makes
a better job than me at tracking my academic papers.
Some of them can also be found on HAL.
Superposition with Structural Induction, Frocos 2017 (preprint)