Mathias Fleury
Titel
Geciteerd door
Geciteerd door
Jaar
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
412018
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
272016
Scalable fine-grained proofs for formula processing
H Barbosa, JC Blanchette, M Fleury, P Fontaine
Journal of Automated Reasoning 64 (3), 485-510, 2020
172020
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
172018
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
132017
Reconstructing veriT proofs in Isabelle/HOL
M Fleury, HJ Schurr
arXiv preprint arXiv:1908.09480, 2019
52019
Optimizing a verified SAT solver
M Fleury
NASA Formal Methods Symposium, 148-165, 2019
52019
Better SMT proofs for easier reconstruction
H Barbosa, J Blanchette, M Fleury, P Fontaine, HJ Schurr
52019
Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL
JC Blanchette, M Fleury, D Traytel
52017
SPASS-SATT
M Bromberger, M Fleury, S Schwarz, C Weidenbach
International Conference on Automated Deduction, 111-122, 2019
42019
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
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
Formalization of logical calculi in Isabelle/HOL
M Fleury
Saarländische Universitäts-und Landesbibliothek, 2020
12020
Formalization of nested multisets, hereditary multisets, and syntactic ordinals
JC Blanchette, M Fleury, D Traytel
Archive of Formal Proofs, 2016
12016
A Verified SAT Solver Framework including Optimization and Partial Valuations.
M Fleury, C Weidenbach
LPAR, 212-229, 2020
2020
Concrete Semantics with Isabelle/HOL
J Blanchette, M Fleury, D Wand
2015
Formal Proof for Gene Clustering
M Fleury, BM Bui-Xuan, F Peschanski
2013
HAL Id: hal-02381819
H Barbosa, J Blanchette, M Fleury, P Fontaine, HJ Schurr
Akshay, S.
S Amani, A Bakhirkin, T Balabonski, H Barbosa, D Burlyaev, PE Camurati, ...
Het systeem kan de bewerking nu niet uitvoeren. Probeer het later opnieuw.
Artikelen 1–20