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, nunchaku.

I completed my PhD after 3 years at Deducteam (INRIA), from October 2012 to September 2015, under the supervision of Gilles Dowek and Guillaume Burel. My work takes place in the field of first-order automated deduction. 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,
then at
EPFL, in Switzerland, where I got a master
degree in **Computer Science**.

I am interested in Artificial Intelligence, formal logic, programming languages; classical music and opéra, science-fiction and more generally by reading.

I used to be a member of the Binet Réseau, 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 theorem proving.
- A 3 months and a half internship at the ProVal lab in INRIA. The topic was about integrating
`TPTP`

provers in the Why software. - 6 months internship in the Computer Science Lab in SRI International.
- 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.

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)
- Satisfiability Modulo Bounded Checking, CADE 2017 (preprint)
- PhD thesis (draft) "Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond", and the sources, under Creative Commons.
- Master thesis on First order reasoning in Yices2
- Detection of First Order Axiomatic Theories and the pre-print version

**Superposition with Structural Induction**(Talk at FroCoS, 2017) slides**Sat Modulo Bounded Checking**(Talk at CADE 26, 2017) slides**Zipperposition, a new platform for Deduction Modulo**(LSV Cachan, 2017) slides**Sat Modulo Bounded Checking**(Talk at VU Amsterdam, 2017) slides**SMBC: Engineering a Fast Solver in OCaml**(Séminaire Ingénieur Inria, 2017 slides)**Superposition+Structural Induction**(at WAIT 2016, Vienna, slides)**Engineering Nunchaku: A Modular Pipeline of Codecs**(Séminaire ingénieur Inria, 2016 slides)**Nunchaku: Flexible Model Finding for Higher-Order Logic**(Montpellier, 2016 slides)**Short Presentation of OCaml**(slides)**Thesis Defense**(slides)**Wedding Boolean Solvers with Superposition: a Societal Reform**, Deducteam seminar, 23rd January 2015 (slides)**Logtk: A Logic Toolkit for Automated Reasoning, and its Implementation**, PAAR 2014, 23 July 2014 (slides)**Sequence: Simple and Efficient Iterators**, OCaml user meeting, 8th July 2014 (slides)**Automated Recognition of First-Order Theories**, Frocos 2013 (slides)

- lectures in MPSI (classes préparatoires) in 2014

I am using several GNU/Linux distributions, currently debian and archlinux. See this page.

Most of the programs I write and maintain nowadays are on my github profile; most are in OCaml. You can also take a look at the documentation of some of the libraries below (might be outdated).

- containers, a modular, ligthweight extension to OCaml's standard library. Doc
- zipperposition, a superposition prover written in OCaml. Doc
- nunchaku, a model finder for higher-order logic, relying on CVC4, Kodkod, Paradox, and smbc (below).
- smbc, a model finder for computational logic with datatypes and recursive functions.
- datalog, a bottom-up datalog engine written in OCaml.
- sequence, a small OCaml library for iterating on containers. Doc
- gen, another style of OCaml iterators
- logtk (
**merged into Zipperposition**), a logic toolkit in OCaml, used in Zipperposition, with many data structures and algorithms.

- qcheck, a QuickCheck inspired property-based testing for OCaml, and combinators to generate random values to run tests on. Doc

- OLinq, an in-memory query language for OCaml
- OCaml-bigstring, an OCaml library to deal with bigarrays of bytes
- maki, an on-disk, content-addressed memoization library for OCaml

- abrasatcuda, a SAT-solver written in C and initially intended to run on CUDA. Written together with Vincent Barrielle as a project for a lecture.
- db2xml.py, a small python script to extract an Android
SMS database (say, after a backup) to a XML file that
SMS backup-restore
can read back.
**NO GUARANTEE**of it working at all, use at your own risk! - deref, an ocaml script to replace symlinks by the content of the file they point to.
- print.py, in python, using
`pycups`

and`cherrypy`

to provide a simple web form to print files

- mail :
`simon[dot]cruanes[dot]2007[at]m4x[dot]org`

- I am on irc (freenode, rezosup) with
`companion_cube`

as nickname. - pgp public key
- a blog friends and me started a while ago (not very active)