Mathias Fleury

According to our database, Mathias Fleury authored at least 29 papers between 2016 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Life span of SAT techniques.

Mathias Fleury, Daniela Kaufmann

CoRR, 2024

IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL.

Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

2023

Automatic Verification of SMT Rewrites in Isabelle/HOL.

Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023) co-located with the 29th International Conference on Automated Deduction (CADE 2023), 2023

Faster LRAT Checking Than Solving with CaDiCaL.

Florian Pollitt, Mathias Fleury, Armin Biere

Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing, 2023

The SAT Museum.

Armin Biere, Mathias Fleury, Nils Froleyks, Marijn J. H. Heule

Proceedings of the 14th International Workshop on Pragmatics of SAT co-located with the 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), 2023

A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper).

Mathias Fleury, Peter Lammich

Proceedings of the Automated Deduction - CADE 29, 2023

2022

Better Decision Heuristics in CDCL through Local Search and Target Phases.

Shaowei Cai, Xindi Zhang, Mathias Fleury, Armin Biere

J. Artif. Intell. Res., 2022

Mining definitions in Kissat with Kittens.

Mathias Fleury, Armin Biere

Formal Methods Syst. Des., 2022

Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses.

Mathias Fleury, Armin Biere

CoRR, 2022

2021

Alethe: Towards a Generic SMT Proof Format (extended abstract).

Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine

Proceedings of the Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, 2021

Abstract: Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant.

Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais

Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021), 2021

Efficient All-UIP Learned Clause Minimization.

Mathias Fleury, Armin Biere

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant.

Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais

Proceedings of the Automated Deduction - CADE 28, 2021

2020

Formalization of logical calculi in Isabelle/HOL.

Mathias Fleury

PhD thesis, 2020

Scalable Fine-Grained Proofs for Formula Processing.

Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine

J. Autom. Reason., 2020

Practical Algebraic Calculus Checker.

Mathias Fleury, Daniela Kaufmann

Arch. Formal Proofs, 2020

Distributed Cube and Conquer with Paracooba.

Maximilian Heisinger, Mathias Fleury, Armin Biere

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2020, 2020

A Verified SAT Solver Framework including Optimization and Partial Valuations.

Mathias Fleury, Christoph Weidenbach

Proceedings of the LPAR 2020: 23rd International Conference on Logic for Programming, 2020

The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus.

Daniela Kaufmann, Mathias Fleury, Armin Biere

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

2019

Reconstructing veriT Proofs in Isabelle/HOL.

Mathias Fleury, Hans-Jörg Schurr

Proceedings of the Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, 2019

Optimizing a Verified SAT Solver.

Mathias Fleury

Proceedings of the NASA Formal Methods - 11th International Symposium, 2019

SPASS-SATT - A CDCL(LA) Solver.

Martin Bromberger, Mathias Fleury, Simon Schwarz, Christoph Weidenbach

Proceedings of the Automated Deduction - CADE 27, 2019

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

A verified SAT solver with watched literals using imperative HOL.

Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017

Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL.

Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel

Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

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, Christian Sternagel, René Thiemann, Dmitriy Traytel

Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

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

Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals.

Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel

Arch. Formal Proofs, 2016

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality.

Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016