Mathias Fleury

41 papers A* 1A 10B 7Journal 11Unranked 10

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	Real-time Proof Checking for Distributed Incremental SAT Solving. TACAS (1) Dominik Schreiber, Mathias Fleury, Katalin Fazekas, Armin Biere
2025	B	`conf`	Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. ITP Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark W. Barrett, Cesare Tinelli
2025	J	`jnl`	Lazy Reimplication in Chronological Backtracking. CoRR Robin Coutelier, Mathias Fleury, Laura Kovács
2025	A	`conf`	Learn to Unlearn. SAT Bernhard Gstrein, Florian Pollitt, André Schidler, Mathias Fleury, Armin Biere
2024	—	`conf`	CaDiCaL 2.0. CAV (1) Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, Florian Pollitt
2024	B	`conf`	Certifying Incremental SAT Solving. LPAR Katalin Fazekas, Florian Pollitt, Mathias Fleury, Armin Biere
2024	A	`conf`	Clausal Congruence Closure. SAT Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks
2024	B	`conf`	Clausal Equivalence Sweeping. FMCAD Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks
2024	—	`conf`	IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. TACAS (1) Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2024	A	`conf`	Lazy Reimplication in Chronological Backtracking. SAT Robin Coutelier, Mathias Fleury, Laura Kovács
2024	J	`jnl`	Life span of SAT techniques. CoRR Mathias Fleury, Daniela Kaufmann
2024	J	`jnl`	Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker. Formal Methods Syst. Des. Daniela Kaufmann, Mathias Fleury, Armin Biere, Manuel Kauers
2023	A	`conf`	A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper). CADE Mathias Fleury, Peter Lammich
2023	—	`conf`	Automatic Verification of SMT Rewrites in Isabelle/HOL. SMT Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2023	A	`conf`	Faster LRAT Checking Than Solving with CaDiCaL. SAT Florian Pollitt, Mathias Fleury, Armin Biere
2023	—	`conf`	The SAT Museum. POS@SAT Armin Biere, Mathias Fleury, Nils Froleyks, Marijn J. H. Heule
2022	J	`jnl`	Better Decision Heuristics in CDCL through Local Search and Target Phases. J. Artif. Intell. Res. Shaowei Cai, Xindi Zhang, Mathias Fleury, Armin Biere
2022	J	`jnl`	Mining definitions in Kissat with Kittens. Formal Methods Syst. Des. Mathias Fleury, Armin Biere
2022	J	`jnl`	Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses. CoRR Mathias Fleury, Armin Biere
2021	—	`conf`	Abstract: Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant. SMT Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais
2021	—	`conf`	Alethe: Towards a Generic SMT Proof Format (extended abstract). PxTP Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine
2021	A	`conf`	Efficient All-UIP Learned Clause Minimization. SAT Mathias Fleury, Armin Biere
2021	—	`ed.`	Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021. PxTP Chantal Keller, Mathias Fleury
2021	A	`conf`	Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant. CADE Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais
2020	B	`conf`	A Verified SAT Solver Framework including Optimization and Partial Valuations. LPAR Mathias Fleury, Christoph Weidenbach
2020	A	`conf`	Distributed Cube and Conquer with Paracooba. SAT Maximilian Heisinger, Mathias Fleury, Armin Biere
2020	—	`—`	Formalization of logical calculi in Isabelle/HOL. Mathias Fleury
2020	J	`jnl`	Practical Algebraic Calculus Checker. Arch. Formal Proofs Mathias Fleury, Daniela Kaufmann
2020	J	`jnl`	Scalable Fine-Grained Proofs for Formula Processing. J. Autom. Reason. Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine
2020	B	`conf`	The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus. FMCAD Daniela Kaufmann, Mathias Fleury, Armin Biere
2019	—	`conf`	Optimizing a Verified SAT Solver. NFM Mathias Fleury
2019	—	`conf`	Reconstructing veriT Proofs in Isabelle/HOL. PxTP Mathias Fleury, Hans-Jörg Schurr
2019	A	`conf`	SPASS-SATT - A CDCL(LA) Solver. CADE Martin Bromberger, Mathias Fleury, Simon Schwarz, Christoph Weidenbach
2018	J	`jnl`	A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. J. Autom. Reason. Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach
2018	B	`conf`	A verified SAT solver with watched literals using imperative HOL. CPP Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich
2017	A*	`conf`	A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. IJCAI Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
2017	—	`conf`	Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS 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
2017	B	`conf`	Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. FSCD Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel
2016	A	`conf`	A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. IJCAR Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
2016	J	`jnl`	Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals. Arch. Formal Proofs Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel
2016	J	`jnl`	Semi-intelligible Isar Proofs from Machine-Generated Proofs. J. Autom. Reason. Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, Albert Steckermeier