Mathias Fleury
Titel
Zitiert von
Zitiert von
Jahr
A verified SAT solver framework with learn, forget, restart, and incrementality
JC Blanchette, M Fleury, P Lammich, C Weidenbach
Journal of automated reasoning 61 (1-4), 333-365, 2018
442018
Semi-intelligible Isar proofs from machine-generated proofs
JC Blanchette, S Böhme, M Fleury, SJ Smolka, A Steckermeier
Journal of Automated Reasoning 56 (2), 155-200, 2016
292016
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
202018
Scalable fine-grained proofs for formula processing
H Barbosa, JC Blanchette, M Fleury, P Fontaine
Journal of Automated Reasoning 64 (3), 485-510, 2020
192020
Foundational (co) datatypes and (co) recursion for higher-order logic
J Biendarra, JC Blanchette, A Bouzy, M Desharnais, M Fleury, J Hölzl, ...
International Symposium on Frontiers of Combining Systems, 3-21, 2017
142017
CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020
A Biere, K Fazekas, M Fleury, M Heisinger
62020
Optimizing a verified SAT solver
M Fleury
NASA Formal Methods Symposium, 148-165, 2019
62019
Better SMT proofs for easier reconstruction
H Barbosa, J Blanchette, M Fleury, P Fontaine, HJ Schurr
62019
SPASS-SATT
M Bromberger, M Fleury, S Schwarz, C Weidenbach
International Conference on Automated Deduction, 111-122, 2019
52019
Reconstructing veriT proofs in Isabelle/HOL
M Fleury, HJ Schurr
arXiv preprint arXiv:1908.09480, 2019
52019
Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL
JC Blanchette, M Fleury, D Traytel
52017
Formalization of Weidenbach’s Automated Reasoning—The Art of Generic Problem Solving (2017)
M Fleury, JC Blanchette
32018
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
32015
Formalization of logical calculi in Isabelle/HOL
M Fleury
Saarländische Universitäts-und Landesbibliothek, 2020
22020
Translation of Proofs Provided by External Provers
M Fleury, J Blanchette
Tech. rep. Techniche Universität München, 2014. url: http://perso. eleves …, 2014
22014
Distributed Cube and Conquer with Paracooba
M Heisinger, M Fleury, A Biere
International Conference on Theory and Applications of Satisfiability …, 2020
12020
A Verified SAT Solver Framework including Optimization and Partial Valuations.
M Fleury, C Weidenbach
LPAR, 212-229, 2020
12020
Formalization of nested multisets, hereditary multisets, and syntactic ordinals
JC Blanchette, M Fleury, D Traytel
Archive of Formal Proofs, 2016
12016
The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus
D Kaufmann, M Fleury, A Biere
2020 Formal Methods in Computer Aided Design (FMCAD), 264-269, 2020
2020
Concrete Semantics with Isabelle/HOL
J Blanchette, M Fleury, D Wand
2015
Das System kann den Vorgang jetzt nicht ausführen. Versuchen Sie es später erneut.
Artikel 1–20