Personal page of Simon Cruanes
I work at Imandra in the USA,
where I help develop a user friendly, powerful proof system based
on computational logic. I started 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;
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.
- 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 developed 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.
Other pages on this site
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.
- An overview of Superposition (Talk at Jetbrains research, 2021) slides
- 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)
GNU/Linux and free software
I am using several GNU/Linux distributions, currently debian and archlinux.
See this page.
Most of the programs I wrote (and, for some of them, maintain)
are on my github profile;
most are in OCaml.
- batsat, a port of minisat in Rust. I did
not write the original port, but I modified it heavily.
- 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.
- iter (formerly "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.
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
an OCaml library to deal with bigarrays of bytes
an on-disk, content-addressed memoization library for OCaml
Old scripts, hacks, and projects
(very old stuff)
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
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
cherrypy to provide a simple web form to print files