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 2023 This year, once again, I submitted IsaSAT to the SAT Competition 2023 (the source code is as always available). According to the results, I did not finish last. However, compared to other solvers, I am trailing in the unsatisfiable instances. I believe that this is due to the fact that I still do not have bounded variable elimination. In the past, I assumed that vivification was also very important, but its importance is now less clear after Daniela and I attempted to examine it more precisely for POS'23 on the SAT solver CaDiCaL. …

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

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

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