Mathias Fleury

ORCID

Publication Activity (10 Years)

Years Active: 2016-2024
Publications (10 Years): 33

Top Venues

Saarland University, Saarbrücken, Germany (PHD)

Education History

Saarland University, Saarbrücken, Germany

PHD

Publications

Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks
Clausal Congruence Closure. SAT (2024)
Katalin Fazekas, Florian Pollitt, Mathias Fleury, Armin Biere
Certifying Incremental SAT Solving. LPAR (2024)
Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, Florian Pollitt
CaDiCaL 2.0. CAV (1) (2024)
Robin Coutelier, Mathias Fleury, Laura Kovács
Lazy Reimplication in Chronological Backtracking. SAT (2024)
Mathias Fleury, Daniela Kaufmann
Life span of SAT techniques. CoRR (2024)
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. TACAS (1) (2024)
Mathias Fleury, Peter Lammich
A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper). CADE (2023)
Florian Pollitt, Mathias Fleury, Armin Biere
Faster LRAT Checking Than Solving with CaDiCaL. SAT (2023)
Armin Biere, Mathias Fleury, Nils Froleyks, Marijn J. H. Heule
The SAT Museum. POS@SAT (2023)
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
Automatic Verification of SMT Rewrites in Isabelle/HOL. SMT (2023)
Mathias Fleury, Armin Biere
Mining definitions in Kissat with Kittens. Formal Methods Syst. Des. 60 (3) (2022)
Shaowei Cai, Xindi Zhang, Mathias Fleury, Armin Biere
Better Decision Heuristics in CDCL through Local Search and Target Phases. J. Artif. Intell. Res. 74 (2022)
Mathias Fleury, Armin Biere
Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses. CoRR (2022)
Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais
Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant. CADE (2021)
Mathias Fleury, Armin Biere
Efficient All-UIP Learned Clause Minimization. SAT (2021)
Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais
Abstract: Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant. SMT (2021)
Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine
Alethe: Towards a Generic SMT Proof Format (extended abstract). PxTP (2021)
Daniela Kaufmann, Mathias Fleury, Armin Biere
The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus. FMCAD (2020)
Maximilian Heisinger, Mathias Fleury, Armin Biere
Distributed Cube and Conquer with Paracooba. SAT (2020)
Mathias Fleury, Daniela Kaufmann
Practical Algebraic Calculus Checker. Arch. Formal Proofs 2020 (2020)
Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine
Scalable Fine-Grained Proofs for Formula Processing. J. Autom. Reason. 64 (3) (2020)
Mathias Fleury, Christoph Weidenbach
A Verified SAT Solver Framework including Optimization and Partial Valuations. LPAR (2020)
Martin Bromberger, Mathias Fleury, Simon Schwarz, Christoph Weidenbach
SPASS-SATT - A CDCL(LA) Solver. CADE (2019)
Mathias Fleury
Optimizing a Verified SAT Solver. NFM (2019)
Mathias Fleury, Hans-Jörg Schurr
Reconstructing veriT Proofs in Isabelle/HOL. PxTP (2019)
Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. J. Autom. Reason. 61 (1-4) (2018)
Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich
A verified SAT solver with watched literals using imperative HOL. CPP (2018)
Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondrej Kuncar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS (2017)
Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. IJCAI (2017)
Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. FSCD (2017)
Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, Albert Steckermeier
Semi-intelligible Isar Proofs from Machine-Generated Proofs. J. Autom. Reason. 56 (2) (2016)
Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals. Arch. Formal Proofs 2016 (2016)
Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. IJCAR (2016)

Mathias Fleury.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Mathias Fleury