Follow
Mathias Fleury
Mathias Fleury
Verified email at informatik.uni-freiburg.de - Homepage
Title
Cited by
Cited by
Year
CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020
A Biere, K Fazekas, M Fleury, M Heisinger
1772020
A verified SAT solver framework with learn, forget, restart, and incrementality
JC Blanchette, M Fleury, P Lammich, C Weidenbach
Journal of automated reasoning 61, 333-365, 2018
692018
Semi-intelligible Isar proofs from machine-generated proofs
JC Blanchette, S Böhme, M Fleury, SJ Smolka, A Steckermeier
Journal of Automated Reasoning 56, 155-200, 2016
362016
Scalable fine-grained proofs for formula processing
H Barbosa, JC Blanchette, M Fleury, P Fontaine
Journal of Automated Reasoning 64 (3), 485-510, 2020
352020
A verified SAT solver with watched literals using imperative HOL
M Fleury, JC Blanchette, P Lammich
Proceedings of the 7th ACM SIGPLAN International Conference on Certified …, 2018
342018
Optimizing a verified SAT solver
M Fleury
NASA Formal Methods: 11th International Symposium, NFM 2019, Houston, TX …, 2019
182019
Foundational (co) datatypes and (co) recursion for higher-order logic
J Biendarra, JC Blanchette, A Bouzy, M Desharnais, M Fleury, J Hölzl, ...
Frontiers of Combining Systems: 11th International Symposium, FroCoS 2017 …, 2017
182017
CaDiCaL, Kissat, Paracooba entering the SAT competition 2021
A Biere, M Fleury, M Heisinger
Proc. of SAT Competition, 10-13, 2021
162021
Distributed cube and conquer with paracooba
M Heisinger, M Fleury, A Biere
Theory and Applications of Satisfiability Testing–SAT 2020: 23rd …, 2020
132020
Reconstructing veriT proofs in Isabelle/HOL
M Fleury, HJ Schurr
arXiv preprint arXiv:1908.09480, 2019
132019
SPASS-SATT: A CDCL (LA) Solver
M Bromberger, M Fleury, S Schwarz, C Weidenbach
Automated Deduction–CADE 27: 27th International Conference on Automated …, 2019
122019
Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant.
HJ Schurr, M Fleury, M Desharnais
CADE 28, 450-467, 2021
112021
Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL
JC Blanchette, M Fleury, D Traytel
FSCD 2017: 2nd International Conference on Formal Structures for Computation …, 2017
112017
Pacheck and Pastèque, checking practical algebraic calculus proofs
D Kaufmann, M Fleury, A Biere
FMCAD 2020 1, 264-269, 2020
92020
Better SMT proofs for easier reconstruction
H Barbosa, JC Blanchette, M Fleury, P Fontaine, HJ Schurr
AITP 2019-4th Conference on Artificial Intelligence and Theorem Proving, 2019
92019
Alethe: Towards a generic SMT proof format
HJ Schurr, M Fleury, H Barbosa, P Fontaine
arXiv preprint arXiv:2107.02354, 2021
82021
Chasing target phases
A Biere, M Fleury
Workshop on the Pragmatics of SAT, 2020
82020
Formalization of logical calculi in Isabelle/HOL
M Fleury
Saarländische Universitäts-und Landesbibliothek, 2020
82020
Formalisation of ground inference systems in a proof assistant
M Fleury, J Blanchette, D Traytel
M. Sc. thesis, École normale supérieure de Rennes, 2015
62015
IsaFoL: Isabelle formalization of logic
JC Blanchette, M Fleury, A Schlichtkrull, D Traytel
URL: https://bitbucket. org/isafol/isafol, 0
5
The system can't perform the operation now. Try again later.
Articles 1–20