| CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020 A Biere, K Fazekas, M Fleury, M Heisinger | 398 | 2020 |
| 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 | 85 | 2018 |
| Scalable fine-grained proofs for formula processing H Barbosa, JC Blanchette, M Fleury, P Fontaine Journal of Automated Reasoning 64 (3), 485-510, 2020 | 45 | 2020 |
| Gimsatul, IsaSAT and Kissat entering the SAT competition 2022 A Biere, M Fleury Proc. of SAT Competition, 10-11, 2022 | 44 | 2022 |
| 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 | 41 | 2018 |
| 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 | 41 | 2016 |
| Optimizing a verified SAT solver M Fleury NASA Formal Methods: 11th International Symposium, NFM 2019, Houston, TX …, 2019 | 31 | 2019 |
| Alethe: Towards a generic SMT proof format HJ Schurr, M Fleury, H Barbosa, P Fontaine arXiv preprint arXiv:2107.02354, 2021 | 21 | 2021 |
| Better decision heuristics in CDCL through local search and target phases S Cai, X Zhang, M Fleury, A Biere Journal of Artificial Intelligence Research 74, 1515-1563, 2022 | 20 | 2022 |
| 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 | 20 | 2017 |
| Distributed cube and conquer with paracooba M Heisinger, M Fleury, A Biere Theory and Applications of Satisfiability Testing–SAT 2020: 23rd …, 2020 | 19 | 2020 |
| Reconstructing veriT proofs in Isabelle/HOL M Fleury, HJ Schurr arXiv preprint arXiv:1908.09480, 2019 | 19 | 2019 |
| Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant. HJ Schurr, M Fleury, M Desharnais CADE 28, 450-467, 2021 | 18 | 2021 |
| SPASS-SATT: A CDCL (LA) Solver M Bromberger, M Fleury, S Schwarz, C Weidenbach Automated Deduction–CADE 27: 27th International Conference on Automated …, 2019 | 16 | 2019 |
| Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL JC Blanchette, M Fleury, D Traytel 2nd International Conference on Formal Structures for Computation and …, 2017 | 14 | 2017 |
| Chasing target phases A Biere, M Fleury Workshop on the Pragmatics of SAT, 2020 | 13 | 2020 |
| CaDiCaL vivinst, IsaSAT, Gimsatul, Kissat, and TabularaSAT entering the SAT competition 2023 A Biere, M Fleury, F Pollitt SAT COMPETITION 2023, 14, 2023 | 11 | 2023 |
| Formalization of logical calculi in Isabelle/HOL M Fleury Saarländische Universitäts-und Landesbibliothek, 2020 | 11 | 2020 |
| Pacheck and Pastèque, checking practical algebraic calculus proofs D Kaufmann, M Fleury, A Biere FMCAD 2020 1, 264-269, 2020 | 10 | 2020 |
| 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 | 10 | 2019 |
Armin BiereProfessor of Computer Science, University of FreiburgVerified email at informatik.uni-freiburg.de
