Personal page of Simon Cruanes
Presentation
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 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.
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 there. 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.
Talks
- 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
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.
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
- zipperposition, a
superposition prover written in OCaml.
- 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
- gen, another style of OCaml iterators
- logtk (merged into Zipperposition), a logic toolkit in OCaml, used in
Zipperposition, with many data structures and algorithms.
Old scripts, hacks, and projects
- gpgforce.py, a small python
script I wrote to find the pgp passphrase I forgot (requires
pyme)
- 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.
- markdownPreprocessor, a small
preprocessor for the
markdown format, which allows
to use LaTeX formulae. It is obviously less powerful and safe than
pandoc, that I am planning
to use from now on.
- 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
Interesting links
Misc
- mail :
simon[dot]cruanes[dot]2007[at]m4x[dot]org
- I am on irc (freenode, rezosup) with
companion_cube as nickname.
- phone number at loria: 03-54-95-85-76
- pgp public key
- a blog friends and me started a while ago (not very active)
- basic vim syntax file for tptp (now superseded by https://github.com/c-cube/vim-tptp)
- OTR fingerprint: 3C39F95D 81EB7EB3 4CE3D09F 6358372D 4C78AC1E
This page uses markdown, and GNU Make.
back to home
