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)

List of the PCs I took part in. I do not include subreviews in the list. 2025 PC of SBMF 2025 PC of CAV 2025 - Artifact Evaluation, 36th International Conference on Computer-Aided Verification PC of FMCAD'25 student forum PC of SAT'25 - The International Conference on Theory and Applications of Satisfiability Testing PC of FroCos - 15th in a series of meetings of the International Symposium on Frontiers of Combining Systems PC of CADE 30 - The Conference on Automated Deduction External reviewer for ITP 2025 - 16th International Conference on Interactive Theorem Proving Review for the journals JAR, JAIR, TCAD PC of TACAS - Artefact Evaluation, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems 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. 2025 Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Andrew Reynolds, Jibiana Jakpor, Bruno Andreotti, Clark Barrett, Hans-Joerg Schurr, and Cesare Tinelli, Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL ITP 2025 Bernhard Gstrein, Florian Pollitt, André Schidler, Mathias Fleury, Armin Biere SAT 2025 paper (open access) Florian Pollitt, Mathias Fleury, Armin Biere, Karem Sakallah, Marijn Heule, Jiawei Chen, and Yonathan Fisseha, Revisiting Clause Vivification POS 2025 paper Katalin Fazekas, Florian Pollitt, Mathias Fleury, and Armin Biere, Incremental Inprocessing Rules beyond Resolution POS 2025 paper 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.

2025 Vice-head of the W2 group proof cost-action (started 2023). 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). 2025 Mathias Fleury, How to consume CaDiCaL proofs Dagstuhl 13051 Slides 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

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.

2025 Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Andrew Reynolds, Jibiana Jakpor, Bruno Andreotti, Clark Barrett, Hans-Joerg Schurr, and Cesare Tinelli, Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL ITP 2025 Bernhard Gstrein, Florian Pollitt, André Schidler, Mathias Fleury, Armin Biere SAT 2025 paper (open access) @inproceedings{GstreinPollittSchidlerFleuryBiere-SAT25, author = {Bernhard Gstrein and Florian Pollitt and Andr{\'{e}} Schidler and Mathias Fleury and Armin Biere}, editor = {Jeremias Berg and Jakob Nordstr{\"{o}}m}, title = {Learn to Unlearn}, booktitle = {28th International Conference on Theory and Applications of Satisfiability Testing, {SAT} 2025, August 12-15, 2025, Glasgow, Scotland}, series = {LIPIcs}, volume = {341}, pages = {14:1--14:12}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2025}, doi = {10.4230/LIPICS.SAT.2025.14}, } Florian Pollitt, Mathias Fleury, Armin Biere, Karem Sakallah, Marijn Heule, Jiawei Chen, and Yonathan Fisseha, Revisiting Clause Vivification POS 2025 paper TODO Katalin Fazekas, Florian Pollitt, Mathias Fleury, and Armin Biere, Incremental Inprocessing Rules beyond Resolution POS 2025 paper TODO 2024 Robin Coutelier, Mathias Fleury and Laura Kovács, Lazy Reimplication in Chronological Backtracking SAT 2024 preprint @InProceedings{coutelier_et_al:LIPIcs.SAT.2024.9, author = {Coutelier, Robin and Fleury, Mathias and Kov\'{a}cs, Laura}, title = {{Lazy Reimplication in Chronological Backtracking}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {9:1--9:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.9}, URN = {urn:nbn:de:0030-drops-205313}, doi = {10.4230/LIPIcs.SAT.2024.9}, annote = {Keywords: Chronological Backtracking, CDCL, Invariants, Watcher Lists} } Armin Biere, Katalin Fazekas, Mathias Fleury and Nils Frolekys, Clausal Congruence Closure SAT 2024 preprint @InProceedings{BiereFazekasFleuryFroleyks-SAT24, author = {Biere, Armin and Fazekas, Katalin and Fleury, Mathias and Froleyks, Nils}, title = {{Clausal Congruence Closure}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {6:1--6:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.6}, URN = {urn:nbn:de:0030-drops-205287}, doi = {10.4230/LIPIcs.SAT.2024.6}, } Armin Biere, Tobias Faller Katalin Fazekas, Mathias Fleury, Nils Froleyks and Florian Pollitt, CaDiCaL 2.0 CAV 2024 paper @inproceedings{BiereFallerFazekasFleuryFroleyks-CAV24, author = {Armin Biere and Tobias Faller and Katalin Fazekas and Mathias Fleury and Nils Froleyks and Florian Pollitt}, editor = {Arie Gurfinkel and Vijay Ganesh}, title = {{CaDiCaL 2.0}}, booktitle = {Computer Aided Verification - 36th International Conference, {CAV} 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {14681}, pages = {133--152}, publisher = {Springer}, year = {2024}, doi = {10.1007/978-3-031-65627-9\_7}, } Katalin Fazekas, Florian Pollitt, Mathias Fleury and Armin Biere, Certifying Incremental SAT Solving LPAR 2024 paper @inprocessing{FazekasPollittFleuryBiere-LPAR24, author = {Katalin Fazekas and Florian Pollitt and Mathias Fleury and Armin Biere}, editor = {Nikolaj S. Bj{\o}rner and Marijn Heule and Andrei Voronkov}, title = {Certifying Incremental {SAT} Solving}, booktitle = {{LPAR} 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024}, series = {EPiC Series in Computing}, volume = {100}, pages = {321--340}, publisher = {EasyChair}, year = {2024}, url = {https://doi.org/10.29007/pdcc}, doi = {10.29007/PDCC}, } Katalin Fazekas, Florian Pollitt, Mathias Fleury, and Armin Biere, Incremental Proofs for Bounded Model Checking. MBMV'24 Preprint @inproceedings{FazekasPollittFleuryBiere-MBMV24, author = {Katalin Fazekas and Florian Pollitt and Mathias Fleury and Armin Biere}, editor = {Wolfgang Kunz} title = {Incremental Proofs for Bounded Model Checking}, booktitle = {27th GMM/ITG/GI Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems (MBMV'24), Kaiserslautern, Germany}, series = {ITG-Fachberichte}, volume = {314}, pages = {133--143}, publisher = {VDE Verlag}, year = {2024}, } Mathias Fleury and Daniela Kaufmann, Lifespan of SAT techniques Arxiv version of POS 23 https://arxiv.org/abs/2402.01202 @misc{fleury2024life, title={Life span of SAT techniques}, author={Mathias Fleury and Daniela Kaufmann}, year={2024}, eprint={2402.01202}, archivePrefix={arXiv}, primaryClass={cs.LO} } 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 @inproceedings{LachnittFleuryEtAlCVC5Rare, author = {Hanna Lachnitt and Mathias Fleury and Leni Aniva and Andrew Reynolds and Haniel Barbosa and Andres N{\"{o}}tzli and Clark W. Barrett and Cesare Tinelli}, editor = {St{\'{e}}phane Graham{-}Lengrand and Mathias Preiner}, title = {Automatic Verification of {SMT} Rewrites in Isabelle/HOL}, booktitle = {Proceedings of the 21st International Workshop on Satisfiability Modulo Theories {(SMT} 2023) co-located with the 29th International Conference on Automated Deduction {(CADE} 2023), Rome, Italy, July, 5-6, 2023}, series = {{CEUR} Workshop Proceedings}, volume = {3429}, pages = {78}, publisher = {CEUR-WS.org}, year = {2023}, url = {https://ceur-ws.org/Vol-3429/abstract14.pdf}, timestamp = {Wed, 05 Jul 2023 16:52:15 +0200}, biburl = {https://dblp.org/rec/conf/smt/LachnittFA0BNBT23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } 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) @inproceedings{BiereFleuryPolitt-SAT-Competition-2023-solvers, author = {Armin Biere and Mathias Fleury and Florian Pollitt}, title = {{CaDiCaL\_vivinst}, {IsaSAT}, {Gimsatul}, {Kissat}, and {TabularaSAT} Entering the {SAT} Competition 2023}, editor = {Tomas Balyo and Nils Froleyks and Marijn Heule and Markus Iser and Matti J{\"a}rvisalo and Martin Suda}, booktitle = {Proc.~of {SAT Competition} 2023 -- Solver and Benchmark Descriptions}, volume = {B-2023-1}, series = {Department of Computer Science Report Series B}, publisher = {University of Helsinki}, year = 2023, keywords = {competition, cadical,kissat,isasat}, pages = {14--15}, } Robin Trüby, Mathias Fleury, and Armin Biere, Verifying Floating-Point Commutativity with GRS SAT Competition 2023 benchmarks (not reviewed) @inproceedings{TrubyFleuryBiere-SAT-Competition-2023-description, author = {Robin Trüby and Mathias Fleury and Armin Biere}, title = {Verifying Floating-Point Commutativity with {GRS}}, editor = {Tomas Balyo and Nils Froleyks and Marijn Heule and Markus Iser and Matti J{\"a}rvisalo and Martin Suda}, booktitle = {Proc.~of {SAT Competition} 2023 -- Solver and Benchmark Descriptions}, volume = {B-2023-1}, series = {Department of Computer Science Report Series B}, publisher = {University of Helsinki}, year = 2023, keywords = {competition}, pages = {53}, } Sonja Gurtner, Lucas Klemmer, Mathias Fleury and Daniel Große, Replacing RISC-V Instructions by Others SAT Competition 2023 benchmarks (not reviewed) @inproceedings{GurtnerKlemmerFleuryGrosse-SAT-Competition-2023-description, author = {Sonja Gurtner and Lucas Klemmer and Mathias Fleury and Daniel Große}, title = {Replacing {RISC-V} Instructions by Others}, editor = {Tomas Balyo and Nils Froleyks and Marijn Heule and Markus Iser and Matti J{\"a}rvisalo and Martin Suda}, booktitle = {Proc.~of {SAT Competition} 2023 -- Solver and Benchmark Descriptions}, volume = {B-2023-1}, series = {Department of Computer Science Report Series B}, publisher = {University of Helsinki}, year = 2023, keywords = {competition}, pages = {54}, } 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 upcoming Florian Politt, Mathias Fleury, and Armin Biere, Faster LRAT Checking than Solving with CaDiCaL SAT23 Preprint LiPiCS upcoming Florian Politt, Mathias Fleury, and Armin Biere, Efficient Proof Checking with LRAT in CaDiCaL (work in progress) MBMV 23 Preprint @inproceedings{lrat-mbmv, author = {Florian Pollitt and Mathias Fleury and Armin Biere}, title = {Efficient Proof Checking with LRAT in CaDiCaL (work in progress)}, editor = {Armin Biere and Daniel Große}, booktitle = {24th {GMM/ITG/GI} Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems, {MBMV} 2023, Freiburg, Germany, March 23-23, 2023}, year = 2023, publisher = {{VDE}}, pages = {64--67}, note = {Accepted} } 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) @misc{FleuryBiere-POS22, title = {Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses}, author = {Fleury, Mathias and Biere, Armin}, editor = {Matti J\"arvisalo and Daniel Le Berre} doi = {10.48550/ARXIV.2207.13577}, url = {https://arxiv.org/abs/2207.13577}, publisher = {arXiv}, year = {2022}, note = {Pragmatics of SAT 22, POS'22} } Shaowei Cai, Xindi Zhang, Mathias Fleury, and Armin Biere, Better Decision Heuristics in CDCL through Local Search and Target Phases FMSD JAIR Accepted @article{DBLP:journals/jair/SubramanianTLC22, author = {Shaowei Cai and Xindi Zhang and Mathias Fleury and Armin Biere}, journal = {J. Artif. Intell. Res.}, title = {Better Decision Heuristics in CDCL through Local Search and Target Phases}, volume = {74}, pages = {1515--1564}, year = {2022}, note = {Accepted}, month = {July}, } 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 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 SAT'21, LNCS …

Artifacts Reviewing I have consistently felt unease about our approach to examining artifacts. Although I have personally reviewed numerous artifacts, I believe that, as a community, we are mistaken in our methods. Weird Errors and Artifact Problems The objective of artifact creation is straightforward: to enable the reproducibility of results by allowing the same code to be run again in the future. This can be achieved by packaging all necessary components in a repository, such as Zenodo, ensuring that everything is self-contained and does not rely on external internet connections. Indeed, this approach seems quite appealing. …