Mathias Fleury

Orcid: 0000-0002-1705-3083

Affiliations:
  • University of Freiburg, Germany


According to our database1, Mathias Fleury authored at least 33 papers between 2016 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Life span of SAT techniques.
CoRR, 2024

IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

Lazy Reimplication in Chronological Backtracking.
Proceedings of the 27th International Conference on Theory and Applications of Satisfiability Testing, 2024

Clausal Congruence Closure.
Proceedings of the 27th International Conference on Theory and Applications of Satisfiability Testing, 2024

Certifying Incremental SAT Solving.
Proceedings of the LPAR 2024: Proceedings of 25th Conference on Logic for Programming, 2024

CaDiCaL 2.0.
Proceedings of the Computer Aided Verification - 36th International Conference, 2024

2023
Automatic Verification of SMT Rewrites in Isabelle/HOL.
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.
Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing, 2023

The SAT Museum.
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).
Proceedings of the Automated Deduction - CADE 29, 2023

2022
Better Decision Heuristics in CDCL through Local Search and Target Phases.
J. Artif. Intell. Res., 2022

Mining definitions in Kissat with Kittens.
Formal Methods Syst. Des., 2022

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

2021
Alethe: Towards a Generic SMT Proof Format (extended abstract).
Proceedings of the Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, 2021

Abstract: Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant.
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.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant.
Proceedings of the Automated Deduction - CADE 28, 2021

2020
Formalization of logical calculi in Isabelle/HOL.
PhD thesis, 2020

Scalable Fine-Grained Proofs for Formula Processing.
J. Autom. Reason., 2020

Practical Algebraic Calculus Checker.
Arch. Formal Proofs, 2020

Distributed Cube and Conquer with Paracooba.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2020, 2020

A Verified SAT Solver Framework including Optimization and Partial Valuations.
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.
Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

2019
Reconstructing veriT Proofs in Isabelle/HOL.
Proceedings of the Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, 2019

Optimizing a Verified SAT Solver.
Proceedings of the NASA Formal Methods - 11th International Symposium, 2019

SPASS-SATT - A CDCL(LA) Solver.
Proceedings of the Automated Deduction - CADE 27, 2019

2018
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality.
J. Autom. Reason., 2018

A verified SAT solver with watched literals using imperative HOL.
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.
Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality.
Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic.
Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

2016
Semi-intelligible Isar Proofs from Machine-Generated Proofs.
J. Autom. Reason., 2016

Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals.
Arch. Formal Proofs, 2016


  Loading...