Dr. Mathias Fleury
Post-Doc
|
For students, before writing me any email about projects (I have gathered a small list of projects here, but the starting point should be our group page), please read my guideline about emails.
Biographical Sketch
I obtained my PhD early 2020. It is about my formalisation of the conflict-driven clause learning and a verification of an implementation of it in the theorem prover Isabelle.
From September 2019 to September 2021, I was working within the JKU AI Project, in the AI LIT project. I continued my work on my fully verified SAT solver IsaSAT, winning the EDA Challenge, but also working on SAT solving.
I moved to the University of Freiburg (following Armin Biere), continuing my work on SAT solving.
Publications
I want to highlight a few publications to show the research topics I am interested in:
-
Better Decision Heuristics in CDCL through Local Search and Target Phases from Shaowei Cai, Xindi Zhang, Mathias Fleury, and Armin Biere. In this paper, we port some of the strength from (incomplete) local search into (complete) SAT solvers.
-
IsaSAT and Kissat entering the EDA Challenge 2021 is the continuing work on the fully verified SAT solver I have started during my PhD thesis in the proof assistant Isabelle/HOL. Since that it became much (much) better and has won the EDA Challenge.
-
I am not only a user of Isabelle/HOL, but also a developer and I try to improve usability. Towards a Generic SMT Proof Format (extended abstract) goes into the direction of a standard proof format for SMT solvers allowing the reconstruction of those proofs, because Isabelle/HOL only trusts proofs that have been checked. If you use Sledgehammer (if not, terrible mistake!) and ever had a proof with
smt (verit), this is the result of this effort (see also the paper Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant).
See the full list.
Talks
See the full list.
Other Links
I have another personal webpage. I exist on Mastodon and Twitter, although I don’t post much.