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
Armin Biere, Katalin Fazekas, Mathias Fleury and Nils Frolekys, Clausal Congruence Closure
Armin Biere, Tobias Faller Katalin Fazekas, Mathias Fleury, Nils Froleyks and Florian Pollitt, CaDiCaL 2.0
Katalin Fazekas, Florian Pollitt, Mathias Fleury and Armin Biere, Certifying Incremental SAT Solving
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
Katalin Fazekas, Florian Pollitt, Mathias Fleury, and Armin Biere, Incremental Proofs for Bounded Model Checking.
Mathias Fleury and Daniela Kaufmann, Lifespan of SAT techniques
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
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)
Florian Politt, Mathias Fleury, and Armin Biere, Faster LRAT Checking than Solving with CaDiCaL
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
Daniela Kaufmann, Mathias Fleury, Armin Biere, and Manuel Kauers, Practical Algebraic Calculus and Nullstellensatz with the Checkers Pacheck and Pastèque and Nuss-Checker
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)
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 |
|
| 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 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, |
|
|
2019
Mathias Fleury. Optimizing a Verified SAT Solver
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 |
|
|
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.