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. 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 (both pages are under construction). 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 . …

As part of my university job, I publish papers, rewiew others, teach, but also do some administrative tasks.

2024 Co-organization of the SAT/SMT/AR Summer School (in Nancy) with Sophie Tourret and Martin Bromberger 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). …