Publications Mathias Fleury


Maximilian Heisinger, Mathias Fleury, Armin Biere. Distributed Cube and Conquer with Paracooba. In Proc. 23rd Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'20), Lecture Notes in Computer Science (LNCS) vol. 12178, pages 114-122, Springer 2020.
[ preprint | bibtex | award | experiments | paracooba ]

Daniela Kaufmann, Mathias Fleury, Armin Biere. The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus. To appear in Proc.  Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'20), 6 pages, IEEE 2020.
[ paper | bibtex | experiments ]

Mathias Fleury, Daniela Kaufmann. Practical Algebraic Calculus Checker. Archive of Formal Proofs Formal Development
[ Archive of Formal Proofs | bibtex | experiments and link to source code ]

Mathias Fleury and Christoph Weidenbach A Verified SAT Solver Framework including Optimization and Partial Valuations. In Elvira Albert and Laura Kovács (editors). LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, vol 73, pages 212--229
[ bibtex | paper ]


Mathias Fleury Optimizing 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

Mathias Fleury and Hans-Jörg Schurr Reconstructing veriT proofs in Isabelle/HOL. PxTP 2019

Best student paper award

Martin Bromberger, Mathias Fleury, Simon Schwarz, and Christoph Weidenbach SPASS-SATT a CDCL(LA) Solver. In Fontaine, P. Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, pp 111--122

Haniel Barbosa, Jasmin Blanchette, Mathias Fleury, and Pascal Fontaine. Scalable fine-grained proofs for formula processing. In J. Autom Reasoning (2019)


Jasmin Blanchette, Mathias Fleury, Peter Lammich, and Christoph Weidenbach A verified SAT solver framework with learn, forget, restart and incrementality. In Journal of Automated Reasonning 61(1–4), pp. 333–365, 2018

Jasmin Blanchette, Mathias Fleury, and Peter Lammich. A Verified SAT Solver with Watched Literals Using Imperative HOL. In Andronick, J., Felty, A. P. (eds.) 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), pp. 158–171, ACM, 2018.


Jasmin Blanchette, Mathias Fleury, Christoph Weidenbach A verified SAT solver framework with learn, forget, restart and incrementality. In In Sierra, C. (ed.) 26th International Joint Conference on Artificial Intelligence (IJCAI-17), pp. 4786–4790,, 2017.

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. Foundational (co)datatypes and (co)recursion for higher-order logic. In In Dixon, C., Finger, M. (eds.) 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017), LNCS 10483, pp. 3–21, Springer, 2017.

Jasmin Blanchette, Mathias Fleury, and Dmitriy Traytel. Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL 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


Best paper Jasmin Blanchette, Mathias Fleury, Christoph Weidenbach A verified SAT solver framework with learn, forget, restart and incrementality. In Olivetti, N. and Tiwari, A. (eds.) 8th International Joint Conference on Automated Reasoning (IJCAR 2016), Springer, 2016.

Jasmin Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, and Albert Steckermeier Semi-intelligible Isar Proofs from Machine-Generated Proofs. In Journal of Automated Reasoning 56(2), pp. 155–200, 2016.,


PhD thesis Formalization of Logical Calculi in Isabelle/HOL

Master's thesis, Formalisation of Ground Inference Systems in a Proof Assistant.

Report on internship during first year master, Translation of Proofs Provided by External Provers.