Personal page of Simon Cruanes

Presentation

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, 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; swing dancing with the Austin Swing Syndicate; 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.

Computer science

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.

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.

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

Logtk : A Logic ToolKit for Automated Reasoning and its Implementation

Talks

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)

Teaching

tar.gz archive of lectures in MPSI (classes préparatoires) in 2014
(archive of) my teaching page for MPSI (classes préparatoires) in 2014

GNU/Linux and free software

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

Programs

Most of the programs I write and maintain nowadays are on my github profile; most are in OCaml.

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

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

Old scripts, hacks, and projects

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

Misc

mail : simon[dot]cruanes[dot]2007[at]m4x[dot]org
I am on irc (libera.chat ~~freenode~~, rezosup) with companion_cube as nickname.
pgp public key
a blog friends and me started a while ago (not very active)
Mastodon
my weeklybeats profile