This webpage contains documents that I generated, like the Isabelle documentation from my PhD thesis. This is the only way to have links which survives changes in my affiliation.

For my publications, please look here; for my academic duties, please look here.

Research

SAT Solver Framework isasatCDCL

As part of my PhD thesis, I developed a framework to formalize SAT solving. I still continue to expend it. It is not a very fast SAT solver, but you are guaranteed that the answer is correct and that there is no overflow happening internally that would compromise correctness.

Please refer to the IsaSAT page for more details.

SAT Solving SAT

I work with Armin Biere on SAT solving. One (rather obvious, but never written down before) result is that the standard minimization algorithm is complete in the sense that it remove all redundant literals (see more details in our SAT'21 paper). The result comes from a completeness theorem on Horn clauses.

Other interests include:

  • parallel cube-and-conquer SAT solving with the SAT solver Paracooba.
  • normal CDCL with our technique coined shrinking that reduces the size of learned clauses without increasing their glue. The technique is orthogonal to minimization. Shrinking shares the cache used for minimization.

Proof Reconstruction

One very useful tool of the interactive theorem prover Isabelle is the interaction with automatic theorem provers living outside. These tools come in two flavours:

  • Sledgehammer: what facts do I need to prove this goal?
  • The smt-tactic: let Isabelle check the proof you found for this goal!

I worked on integrated veriT into Sledgehammer during my master thesis, but I am now mostly focusing on the second approach. I have extended the tactic to include the SMT solver veriT and I am now working on integrating the SMT solver cvc5 – and unlike the work to integrate the Z3 in Isabelle by Böhme, the authors of cvc5 (especially Barbosa and Lachnitt) and veriT (especially Schurr) are helping me to make the proofs nicer and the reconstruction work easier!

In this direction, several people (including me) are attempting to define a proof format tentatively called Alethe that makes reconstruction easy enough.

LPAC Checking lpacpastèque

With Daniela Kaufmann, we worked on (L)PAC checker, one unverified PACheck and Pastèque verified in Isabelle. Please refer to this page for more details.

Software softwareisasat

See [[./src/sources.org]].

(Newest first!)

Starting October I will be in Freiburg (see my page there), still with Armin Biere.

My current webpage can be found at http://fmv.jku.at/fleury/index.html. This page might or might not be more up-to-date than this one.

Before that I did my PhD at the MPI in Saarbrücken, Germany. My webpage there still exists, because I am still partially affiliated with the MPI.

PhD Thesis thesis

My thesis comes with some fancy Isabelle documentation available here and it would be too bad for the links to get lost. The documentation refers to the fleury-thesis branch of IsaFoL available at https://bitbucket.org/isafol/isafol/wiki/Home

Other Projects

Isabelle/emacs

I work in my free time on Isabelle-emacs available at https://github.com/m-fleury/isabelle-emacs/. It slightly extends Isabelle’s LSP server (no change is done to Isabelle’s kernel nor to Isabelle/jEdit) and make Isabelle usable for Emacs. If you don’t like Isabelle/jEdit or find it unstable and unusable, this provides an alternative.

veriT and SPASS

Sometimes I try to implement some SAT techniques into the SAT solvers veriT and SPASS-SAT used in the SMT solver SPASS-SATT