
Mathias Fleury
Physical location: Campus E1 5, Room 640 (6th floor)
+49 681 9325 - 2931, fax - 2999
Max-Planck-Institut für Informatik
Saarland Informatics Campus
Building E1 4
66123 Saarbrücken
Academic Activity
Research Interest:
- Theorem proving
- Formal verification
Education:
- Starting September 19: postdoc at JKU in Linz, Austria
- September 15 - end of August 19: Ph. D. student at the Max-Planck-Insitut für Informatik and Saarbrücken Graduate School of Computer Science;
- 2013 - 2015: Master at the École Normale Supérieure de Rennes (Brittany, France);
- 2013: Bachelor at the École Normale Supérieure de Rennes (Brittany, France) (former École Normale Supérieur de Cachan, Brittany extension).
Internships:
- February - June 2015: Formalisation of the resolution, DPLL and CDCL calculi, based on Christoph Weidenbach's upcoming textbook Automated Reasoning — The Art of Generic Problem Solving. Master Thesis.
- Summer 2014: Sledgehammer is a powerful interface from Isabelle to automated provers, to discharge subgoals that appear during the interactive proofs. It chooses facts related to this goal and asks some automatic provers to find a proof. The proof can be either reconstructed or just used to extract the relevant lemmas: in both cases the proof is not trusted. We extend the support by adding one first-order prover (Zipperposition), the reconstruction for two higher-order ATPs (Leo-II and Satallax) and an SMT solver veriT. The support of higher-order prover should especially improve Sledgehammer's performance for higher-order goals. This internship project took place at the TUM, under the supervision of Jasmin Blanchette. Report.
- Summer 2013: We present a formalization proof of Uno and Yagiura's algorithm, using the theorem proof assistant Coq. This is a fundamental combinatorial algorithm which operates over permutation. Direct applications include computational biology (e.g. heuristics in estimating the genealogical distance between two species), text processing (e.g. generating the synchronous context-free grammar of two sequences with many-to-many alignment links ), the problem has been generalized to d permutations by Heber and Stoye, ... This internship project took place at LIP6, Université Pierre & Marie Curie, Paris, under the joint supervision of B.M. Bui-Xuan and F. Peschanski.
Draft and Publications
Draft
A Verified SAT Solver Framework including Optimization and Partial Valuations
Mathias Fleury, Christoph Weidenbach, and Dominik Zimmer
Draft PaperFormalizing logical calculi in Isabelle
(submitted)
Latest draft
Journal Papers
- Scalable fine-grained proofs for formula processing
Haniel Barbosa, Jasmin Blanchette, Mathias Fleury, and Pascal Fontaine.
Accepted in Journal of Automated Reasoning (2019)
Preprint (PDF), Springer web page - A verified SAT solver framework with learn, forget, restart, and incrementality
Jasmin Blanchette, Mathias Fleury, Peter Lammich, and Christoph Weidenbach.
Journal of Automated Reasonning 61(1–4), pp. 333–365, 2018
Preprint (PDF) Postprint (Open Access) - Semi-intelligible Isar Proofs from Machine-Generated Proofs
Jasmin Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, and Albert Steckermeier
Journal of Automated Reasoning 56(2), pp. 155–200, 2016
Preprint (PDF), Springer web page
Conference & Workshop Papers
SPASS-SATT a CDCL(LA) Solver
In Pascal Fontaine, CADE-27 (Best Student Paper Award)
Martin Bromberger, Mathias Fleury, Simon Schwarz, and Christoph WeidenbachReconstructing veriT proofs in Isabelle/HOL
Accepted at PxTP 2019
Mathias Fleury and Hans-Jörg Schurr
PreprintOptimizing a Verified SAT Solver
In Badger, J. and Rozier, K.Y (eds). Nasa Formal Methods (NFM 2019), pp. 148-165, Springer, Cham, 2019.
Mathias Fleury
Draft Paper Postprint- A Verified SAT Solver with Watched Literals Using Imperative HOL
Mathias Fleury, Jasmin Blanchette, and Peter Lammich.
In Andronick, J., Felty, A. P. (eds.) 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), pp. 158–171, ACM, 2018.
(PDF) - Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL
Jasmin Blanchette, Mathias Fleury, and Dmitriy Traytel.
In Miller, D. (ed.) 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), LIPIcs 84, pages 11:1–11:18, Schloss Dagstuhl, Leibniz Zentrum für Informatik, 2017,
Postprint (PDF) - Foundational (co)datatypes and (co)recursion for higher-order logic
Julian Biendarra, Jasmin Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, and Dmitriy Traytel.
In Dixon, C., Finger, M. (eds.) 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017), LNCS 10483, pp. 3–21, Springer, 2017. - A verified SAT solver framework with learn, forget, restart, and incrementality
Jasmin Blanchette, Mathias Fleury, and Christoph Weidenbach.
In Sierra, C. (ed.) 26th International Joint Conference on Artificial Intelligence (IJCAI-17), pp. 4786–4790, ijcai.org, 2017.
Postprint (PDF) - A verified SAT solver framework with learn, forget, restart and incrementality
Jasmin Blanchette, Mathias Fleury, and Christoph Weidenbach.
In Olivetti, N. and Tiwari, A. (eds.) 8th International Joint Conference on Automated Reasoning (IJCAR 2016), Springer, 2016.
Preprint (PDF), Springer web page
Workshop Abstracts
- A Verified SAT Solver with Watched Literals Using Imperative HOL,
Mathias Fleury, Jasmin Blanchette, and Peter Lammich.
Isabelle Workshop 2018 - A verified SAT solver framework with learn, forget, restart and incrementality
Jasmin Blanchette, Mathias Fleury, and Christoph Weidenbach.
Isabelle Workshop 2016
Formal Proofs
- Formalization of nested multisets, hereditary multisets, and syntactic ordinals
Jasmin Blanchette, Mathias Fleury, and Dmitriy Traytel. Archive of Formal Proofs, 2016.
Web page
Tutorial
- Programming and Reasoning with Infinite Data in Isabelle/HOL.
Mathias Fleury, Andreas Lochbihler and Andrei Popescu
POP2018 TutorialFest
Internship Reports
- Formalisation of Ground inference Systems in a Proof Assistant, Master Thesis (second year), MPI-Inf
- Translation of Proofs Provided by External Provers, Internship report (first year master), TUM