As part of my university job at the University Freiburg, I publish papers, rewiew others, teach, but also do some administrative tasks. I am currently working on my habilitation (you can find a draft here)

SAT Competition 2024 There is not much to tell for the release for this year of the SAT Competition 2024. This year, I finished last, exactly as expected. However, I am very close to the second-to-last on SAT benchmarks. My main performance problem seems to be UNSAT problems, which I blame on missing preprocessing. I intended to implement variable elimination based on the model reconstruction implemented in Katharina Wagner’s Master’s thesis in Isabelle. I actually started to implement it, but, as usual, once I went to proofs, things became more complicated. But it is interesting. …

List of the PCs I took part in. I do not include subreviews in the list. 2024 Chair of iFM-AE PC of CAV 2024 - Artifact Evaluation, 35th International Conference on Computer-Aided Verification 2023 PC of SBMF 2023 PC of Frocos 2023 PC of FMCAD'23 PC of FMCAD'23 student forum PC of iFM artefact evaluation PC of CAV 2023 - Artifact Evaluation, 34th International Conference on Computer-Aided Verification Review for Mathematics in Computer Science 2022 PC of the stundent forum of FMCAD22, Formal Methods in Computer-Aided Design PC of CAV 2022 - Artifact Evaluation, 34th International Conference on Computer-Aided Verification PC of IJCAR 2022 - International Joint Conference on Automated Reasoning PC of TACAS - Artefact Evaluation, 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2021 Co-chair of PxTP 2021, Seventh Workshop on Proof eXchange for Theorem Proving Review for Journal of Artificial Intelligence PC of CAV 2021 - Artifact Evaluation, 33rd International Conference on Computer-Aided Verification PC of PDAR-21, Parallel and Distributed Automated Reasoning 2021 PC of TACAS - Artefact Evaluation, 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2020 PC of TAP 20 - Artefact Evaluation, 14th International Conference on Tests and Proofs 20 PC of VMCAI-20 - Artefact Evaluation, 21st International Conference on Verification, Model Checking, and Abstract Interpretation 2019 PC of PxTP 2019, Seventh Workshop on Proof eXchange for Theorem Proving

This webpage is also available as long version with the bibtex entries. 2024 Robin Coutelier, Mathias Fleury and Laura Kovács, Lazy Reimplication in Chronological Backtracking SAT 2024 preprint Armin Biere, Katalin Fazekas, Mathias Fleury and Nils Frolekys, Clausal Congruence Closure SAT 2024 preprint Armin Biere, Tobias Faller Katalin Fazekas, Mathias Fleury, Nils Froleyks and Florian Pollitt, CaDiCaL 2.0 CAV 2024 paper Katalin Fazekas, Florian Pollitt, Mathias Fleury and Armin Biere, Certifying Incremental SAT Solving LPAR 2024 paper Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark Barrett, and Cesare Tinelli, IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL TACAS'24 Preprint Katalin Fazekas, Florian Pollitt, Mathias Fleury, and Armin Biere, Incremental Proofs for Bounded Model Checking. MBMV'24 Preprint Mathias Fleury and Daniela Kaufmann, Lifespan of SAT techniques Arxiv version of POS 23 https://arxiv.org/abs/2402.01202 2023 Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Noetzli, Clark W. Barrett and Cesare Tinelli, Automatic Verification of {SMT} Rewrites in Isabelle/HOL SMT Workshop 2023 Abstract Armin Biere, Mathias Fleury, and Florian Pollitt, CaDiCaL_vivinst, IsaSAT, Gimsatul, Kissat, and TabularaSAT Entering the SAT Competition 2023 SAT Competition 2023 system description (not reviewed) Robin Trüby, Mathias Fleury, and Armin Biere, Verifying Floating-Point Commutativity with GRS SAT Competition 2023 benchmarks (not reviewed) Sonja Gurtner, Lucas Klemmer, Mathias Fleury and Daniel Große, Replacing RISC-V Instructions by Others SAT Competition 2023 benchmarks (not reviewed) Mathias Fleury and Peter Lammich, A more Pragmatic CDCL for IsaSAT and targetting LLVM (Short Paper) CADE 29 Preprint Springer (OA, upcoming) 29th International Conference on Automated Deduction Florian Politt, Mathias Fleury, and Armin Biere, Efficient Proof Checking with LRAT in CaDiCaL (work in progress) MBMV 23 Preprint Florian Politt, Mathias Fleury, and Armin Biere, Faster LRAT Checking than Solving with CaDiCaL SAT23 Preprint LiPiCS Mathias Fleury and Daniela Kaufmann, Lifespan of SAT techniques POS 23 Pragmatics of SAT 23 Accepted (POS has no proceedings) Armin Biere , Mathias Fleury , Nils Froleyks and Marijn Heule . The SAT Museum POS 23 Pragmatics of SAT 23 Accepted (POS has no proceedings) 2022 Mathias Fleury and Armin Biere, Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses POS 22 arXiV Pragmatics of SAT 22 Accepted (POS has no proceedings) Shaowei Cai, Xindi Zhang, Mathias Fleury, and Armin Biere, Better Decision Heuristics in CDCL through Local Search and Target Phases FMSD JAIR Accepted Daniela Kaufmann, Mathias Fleury, Armin Biere, and Manuel Kauers, Practical Algebraic Calculus and Nullstellensatz with the Checkers Pacheck and Pastèque and Nuss-Checker FMSD Preprint Springer Accepted 2021 Mathias Fleury and Armin Biere, Efficient All-UIP Learned Clause Minimization SAT'21, LNCS Preprint Springer Proc. 24rd Intl. Conf. on Theory and Applications of Satisfiability Testing Mathias Fleury and Armin Biere, Efficient All-UIP Learned Clause Minimization (Extended Version) Technical Report PDF JKU ePUB Hans-Jörg Schurr, Mathias Fleury, and Martin Desharnais, Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant CADE 28 Springer (Open Access) 28th International Conference on Automated Deduction Mathias Fleury, IsaSAT and Kissat entering the EDA Challenge 2021 Submitted to the EDA Challenge 2021 PDF Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, and Pascal Fontaine Alethe: Towards a Generic SMT Proof Format (extended abstract) PxTP'21 PDF EPTCS Proof Exchange on Theorem Proving 2020 Maximilian Heisinger, Mathias Fleury, and Armin Biere, Distributed Cube and Conquer with Paracooba SAT'20, LNCS Preprint Springer Proc. 23rd Intl. Conf. on Theory and Applications of Satisfiability Testing Daniela Kaufmann, Mathias Fleury, and Armin Biere. The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus FMCAD'20 Preprint IEEE Proc. Intl. Conf. on Formal Methods in Computer Aided Design Mathias Fleury and Daniela Kaufmann. Practical Algebraic Calculus Checker. Archive of Formal Proofs Formal Development AFP AFP entry Archive of Formal Proofs Mathias Fleury and Christoph Weidenbach. A Verified SAT Solver Framework including Optimization and Partial Valuations LPAR-23 PDF EasyChair 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Mathias Fleury, Formalization of Logical Calculi in Isabelle/HOL (PhD thesis) PhD thesis PDF University of Saarland 2019 Mathias Fleury. Optimizing a Verified SAT Solver NFM-19 Preprint Springer NASA Formal Methods - 11th International Symposium Mathias Fleury and Hans-Jörg Schurr, Reconstructing veriT proofs in Isabelle/HOL. PxTP 2019 Arxiv Sixth Workshop on Proof eXchange for Theorem Proving Martin Bromberger, Mathias Fleury, Simon Schwarz, and Christoph Weidenbach, SPASS-SATT a CDCL(LA) Solver. CADE 27 Springer HAL 27th International Conference on Automated Deduction Haniel Barbosa, Jasmin Blanchette, Mathias Fleury, and Pascal Fontaine. Scalable fine-grained proofs for formula processing. JAR 20 Springer HAL Journal of Automated Reasonning 2018 Jasmin Blanchette, Mathias Fleury, Peter Lammich, and Christoph Weidenbach. A verified SAT solver framework with learn, forget, restart and incrementality JAR 18 Springer (Open Access) Journal of Automated Reasonning Jasmin Blanchette, Mathias Fleury, and Peter Lammich. A Verified SAT Solver with Watched Literals Using Imperative HOL. CPP 18 ACM Matryoshka 7th ACM SIGPLAN International Conference on Certified Programs and Proofs 2017 Jasmin Blanchette, Mathias Fleury, Christoph Weidenbach. A verified SAT solver framework with learn, forget, restart and incrementality. IJCAI 17 IJCAI Twenty-Sixth International Joint Conference on Artificial Intelligence 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. FroCoS 2017 ACM Matryoshka 11th International Symposium on Frontiers of Combining Systems Jasmin Blanchette, Mathias Fleury, and Dmitriy Traytel. Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL 2016 Jasmin Blanchette, Mathias Fleury, Christoph Weidenbach. A verified SAT solver framework with learn, forget, restart and incrementality Jasmin Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, and Albert Steckermeier. Semi-intelligible Isar Proofs from Machine-Generated Proofs.

2024 Co-organization of the SAT/SMT/AR Summer School (in Nancy) with Sophie Tourret and Martin Bromberger Vice-head of the W2 group proof cost-action (started 2023). 2023 Vice-head of the W2 group proof cost-action. Committee for the Embedded System Professorship from the University Freiburg IAAA accreditation committee for the Frankreich-Zentrum from the University Freiburg

On this page, I list all my talks and slides. Remark that several talks are impossible to understand without me talking (this is half of the point of the talk: someone is talking). 2024 Mathias Fleury and Bruno Andreotti Alethe, A flexible proof format with fine-grained steps Proof Systems for Mathematics and Verification 2023 Mathias Fleury, in front the Professors (informal talk, towards the habilitation) SAT Solvers: Verify, Improve, And Use Them In Interactive Theorem Provers Mathias Fleury and Peter Lammich, Porting IsaSAT to LLVM (and Inprocessing) Porting IsaSAT to LLVM (and Inprocessing) Mathias Fleury, MDX Isabelle Summer School SMT Reconstruction, shortened Checkers and solvers 2022 Mathias Fleury, Verifying Solvers: How Much Do You Want to Prove? Dagstuhl 22411 Dagstuhl Report Slides Mathias Fleury, Discussion: How to compare techniques in solvers? And how to write such a solver? (work-in-progress with Armin Biere and Karem Sakallah) Dagstuhl 22411 Dagstuhl Report Slides 2021 Mathias Fleury and Armin Biere, Efficient All-UIP Learned Clause Minimization. SAT 2021 video Mathias Fleury and Christoph Weidenbach. A Verified SAT Solver Framework including Optimization and Partial Valuations LPAR-23 slides 2020 Armin Biere and Mathias Fleury, Chasing Target Phases POS'20 slides 11th Workshop on Pragmatics of SAT (POS'20) video Mathias Fleury, One Thousand and One Refinement: From CDCL to a Verified SAT Solver PhD Defense slides 2019 Reconstructing veriT proofs in Isabelle/HOL UPSCaLe meeting slides Paris, November 29, 2019 Fleury and Weidenbach, Extending an Isabelle Formalisation of CDCL to Optimising CDCL Matryoshka Workshop Slides 2018 Blanchette, Fleury, Lammich, and Weidenbach, A Verified SAT Solver with Watched Literals Using Imperative HOL FSCD 2017 slides Fleury, Blanchette, and Fleury, A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract) Matryoshka Workshop Slides 2017 Blanchette, Fleury, and Traytel, Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL FSCD 2017 slides Blanchette, Fleury, Lammich, and Weidenbach, A Verified SAT Solver with Watched Literals Using Imperative HOL PART 2017 slides Blanchette, Fleury, and Weidenbach, A Verified SAT Solver Framework IJCAI 2017 slides 2015 Fleury, Formalisation of Ground Inference Systems in Isabelle GeoCAL 2015 slides

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

Here the release of my projects that I manage myself (so unlike my changes to, e.g., CaDiCaL). IsaSAT 2021: EDA Challenge This the first official release of the IsaSAT in LLVM IR. See the sources and the system description submitted at the EDA Challenge for a list of changes compared to IsaSAT in Standard ML. The main difference compared to the Standard ML version developped in my PhD is that the Isabelle theorem is now incomplete (this was implicit earlier in the sense that it is a limit of the compiler, not a limit of the program) and that the new version is much faster. …

IsaSAT is one of the few verified SAT solvers (and to my knowledge the only one that is currently maintained). It is verified in Isabelle using the Isabelle Refinement Framework by synthesizing code. See the presentation for more details.

As part of my PhD thesis, I developed a framework to formalize SAT solving. I still continue to expand it. The general organization is given by the following graph: . If you want to have a look at the sources, look at the IsaFoL repository (this is the latest bleeding age version, so it is sometimes broken) and the Isabelle-generated HTML documentation (look at the “IsaFoL” version at the bottom to know the corresponding git ID). …