[  21 | 20 | 19 | 18 | 17 | 16 | thesis ]

2021

Mathias Fleury and Armin Biere. Efficient All-UIP Learned Clause Minimization. In Proc. 24rd Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'21), pages 171-187, volume 12831, Lecture Notes in Computer Science (LNCS) Springer 2021
[ preprint | bibtex | extended version | bibtex ]

Mathias Fleury IsaSAT and Kissat entering the EDA Challenge 2021 Submitted to the EDA-Challenge
[ PDF ]

Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, and Pascal Fontaine Alethe: Towards a Generic SMT Proof Format (extended abstract) In Chantal Keller and Mathias Fleury: Proceedings Seventh Workshop on Proof eXchange for Theorem Proving (PxTP 2021), Pittsburgh, USA, 11th July 2021, Electronic Proceedings in Theoretical Computer Science 336, pp. 49–54.
[ PDF (open access) | bib ]

Hans-Jörg Schurr, Mathias Fleury, and Martin Desharnais Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant In André Platzer and Geoff Sutcliffe. Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Pittsburgh, USA, July 12-15, 2021, to appear
[ preprint | Springer page (open access) | Video for the SMT workshop | Abstract at the SMT workshop ]

2020

Maximilian Heisinger, Mathias Fleury, and 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, and 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 and 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 ]

2019

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)

2018

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.

2017

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, ijcai.org, 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

2016

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

Thesis

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.