Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals. - Jasmin Christian Blanchette; Mathias Fleury; Dmitriy Traytel (Arch. Formal Proofs, 2016)

Semi-intelligible Isar Proofs from Machine-Generated Proofs. - Jasmin Christian Blanchette; Sascha Böhme; Mathias Fleury; Steffen Juilf Smolka; Albert Steckermeier (J. Autom. Reason., 2016)

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. - Julian Biendarra; Jasmin Christian Blanchette; Aymeric Bouzy; Martin Desharnais; Mathias Fleury; Johannes Hölzl; Ondrej Kuncar; Andreas Lochbihler; Fabian Meier; Lorenz Panny; Andrei Popescu 001; Christian Sternagel; et al. (FroCoS, 2017)

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. - Jasmin Christian Blanchette; Mathias Fleury; Christoph Weidenbach (IJCAI, 2017)

Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. - Jasmin Christian Blanchette; Mathias Fleury; Dmitriy Traytel (FSCD, 2017)

A verified SAT solver with watched literals using imperative HOL. - Mathias Fleury; Jasmin Christian Blanchette; Peter Lammich (CPP, 2018)

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. - Jasmin Christian Blanchette; Mathias Fleury; Peter Lammich; Christoph Weidenbach (J. Autom. Reason., 2018)

SPASS-SATT - A CDCL(LA) Solver. - Martin Bromberger; Mathias Fleury; Simon Schwarz; Christoph Weidenbach (CADE, 2019)

Optimizing a Verified SAT Solver. - Mathias Fleury (NFM, 2019)

Reconstructing veriT Proofs in Isabelle/HOL. - Mathias Fleury; Hans-Jörg Schurr (PxTP, 2019)

The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus. - Daniela Kaufmann; Mathias Fleury; Armin Biere (FMCAD, 2020)

A Verified SAT Solver Framework including Optimization and Partial Valuations. - Mathias Fleury; Christoph Weidenbach (LPAR, 2020)

Distributed Cube and Conquer with Paracooba. - Maximilian Heisinger; Mathias Fleury; Armin Biere (SAT, 2020)

Practical Algebraic Calculus Checker. - Mathias Fleury; Daniela Kaufmann (Arch. Formal Proofs, 2020)

Scalable Fine-Grained Proofs for Formula Processing. - Haniel Barbosa; Jasmin Christian Blanchette; Mathias Fleury; Pascal Fontaine (J. Autom. Reason., 2020)

Formalization of logical calculi in Isabelle/HOL. - Mathias Fleury (2020)

Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant. - Hans-Jörg Schurr; Mathias Fleury; Martin Desharnais (CADE, 2021)

Efficient All-UIP Learned Clause Minimization. - Mathias Fleury; Armin Biere (SAT, 2021)

Abstract: Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant. - Hans-Jörg Schurr; Mathias Fleury; Martin Desharnais (SMT, 2021)

Alethe: Towards a Generic SMT Proof Format (extended abstract). - Hans-Jörg Schurr; Mathias Fleury; Haniel Barbosa; Pascal Fontaine (PxTP, 2021)

Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses. - Mathias Fleury; Armin Biere (CoRR, 2022)

Mining definitions in Kissat with Kittens. - Mathias Fleury; Armin Biere (Formal Methods Syst. Des., 2022)

Better Decision Heuristics in CDCL through Local Search and Target Phases. - Shaowei Cai 001; Xindi Zhang; Mathias Fleury; Armin Biere (J. Artif. Intell. Res., 2022)

A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper). - Mathias Fleury; Peter Lammich (CADE, 2023)

The SAT Museum. - Armin Biere; Mathias Fleury; Nils Froleyks; Marijn J. H. Heule (POS@SAT, 2023)

Faster LRAT Checking Than Solving with CaDiCaL. - Florian Pollitt; Mathias Fleury; Armin Biere (SAT, 2023)

Automatic Verification of SMT Rewrites in Isabelle/HOL. - Hanna Lachnitt; Mathias Fleury; Leni Aniva; Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (SMT, 2023)

The SAT Museum POS'23 Artifact. - Armin Biere; Mathias Fleury; Nils Froleyks; Marijn Heule (Zenodo, 2023)

IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. - Hanna Lachnitt; Mathias Fleury; Leni Aniva; Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (Zenodo, 2023)

CaDiCaL 2.0. - Armin Biere; Tobias Faller; Katalin Fazekas; Mathias Fleury; Nils Froleyks; Florian Pollitt (CAV (1), 2024)

Clausal Equivalence Sweeping. - Armin Biere; Katalin Fazekas; Mathias Fleury; Nils Froleyks (FMCAD, 2024)

Certifying Incremental SAT Solving. - Katalin Fazekas; Florian Pollitt; Mathias Fleury; Armin Biere (LPAR, 2024)

Clausal Congruence Closure. - Armin Biere; Katalin Fazekas; Mathias Fleury; Nils Froleyks (SAT, 2024)

Lazy Reimplication in Chronological Backtracking. - Robin Coutelier; Mathias Fleury; Laura Kovács (SAT, 2024)

IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. - Hanna Lachnitt; Mathias Fleury; Leni Aniva; Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (TACAS (1), 2024)

Life span of SAT techniques. - Mathias Fleury; Daniela Kaufmann (CoRR, 2024)

CaDiCaL 2.0 CAV'24 Tool-Paper Artifact. - Armin Biere; Tobias Faller; Katalin Fazekas; Mathias Fleury; Nils Froleyks; Florian Pollitt (Zenodo, 2024)

CNF Encoded Isomorphic and Optimized Miters from Hardware Model Checking Competition 2020 Models. - Armin Biere; Katalin Fazekas; Mathias Fleury; Nils Froleyks (Zenodo, 2024)

Clausal Equivalence Sweeping Paper Logs. - Armin Biere; Katalin Fazekas; Mathias Fleury; Nils Froleyks (Zenodo, 2024)

arminbiere/cadical. - Mathias Fleury (DROPS Artifacts, 2024)

m-fleury/glucose. - Mathias Fleury (DROPS Artifacts, 2024)

Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker. - Daniela Kaufmann; Mathias Fleury; Armin Biere; Manuel Kauers (Formal Methods Syst. Des., 2024)

Learn to Unlearn. - Bernhard Gstrein; Florian Pollitt; André Schidler; Mathias Fleury; Armin Biere (SAT, 2025)

CaDiCaL 2.2 System Description Artifact. - Florian Pollitt; Mathias Fleury; Katalin Fazekas; Nils Froleyks; Armin Biere (Zenodo, 2025)

CaDiCaL 2.2 System Description Artifact. - Florian Pollitt; Mathias Fleury; Katalin Fazekas; Nils Froleyks; Armin Biere (Zenodo, 2025)

CaDiCaL 2.2 System Description Artifact. - Florian Pollitt; Mathias Fleury; Katalin Fazekas; Nils Froleyks; Armin Biere (Zenodo, 2025)