I work at Inria Nancy 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 there. 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
- Tool Integration with the Evidential Tool Bus (springerlink). The pre-print version is available here.
- Detection of First Order Axiomatic Theories and the pre-print version
- Logtk : A Logic ToolKit for Automated Reasoning and its Implementation

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

- 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

- La quadrature du Net, a french association that defends net neutrality.
- lambda the ultimate, a blog on (functional) programming languages

- 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