| CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020 A Biere, K Fazekas, M Fleury, M Heisinger | 434 | 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 | 88 | 2018 |
| Gimsatul, IsaSAT and Kissat entering the SAT competition 2022 A Biere, M Fleury Proc. of SAT Competition, 10-11, 2022 | 51 | 2022 |
| Scalable fine-grained proofs for formula processing H Barbosa, JC Blanchette, M Fleury, P Fontaine Journal of Automated Reasoning 64 (3), 485-510, 2020 | 46 | 2020 |
| 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 | 43 | 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 | 43 | 2016 |
| Optimizing a verified SAT solver M Fleury NASA Formal Methods: 11th International Symposium, NFM 2019, Houston, TX …, 2019 | 32 | 2019 |
| 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 | 25 | 2022 |
| Alethe: Towards a generic SMT proof format HJ Schurr, M Fleury, H Barbosa, P Fontaine arXiv preprint arXiv:2107.02354, 2021 | 23 | 2021 |
| Reconstructing veriT proofs in Isabelle/HOL M Fleury, HJ Schurr arXiv preprint arXiv:1908.09480, 2019 | 21 | 2019 |
| Distributed cube and conquer with paracooba M Heisinger, M Fleury, A Biere Theory and Applications of Satisfiability Testing–SAT 2020: 23rd …, 2020 | 20 | 2020 |
| 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 |
| Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant. HJ Schurr, M Fleury, M Desharnais CADE 28, 450-467, 2021 | 19 | 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 |
| CaDiCaL 2.0 A Biere, T Faller, K Fazekas, M Fleury, N Froleyks, F Pollitt International Conference on Computer Aided Verification, 133-152, 2024 | 15 | 2024 |
| Chasing target phases A Biere, M Fleury Workshop on the Pragmatics of SAT, 2020 | 14 | 2020 |
| 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 |
| CaDiCaL vivinst, IsaSAT, Gimsatul, Kissat, and TabularaSAT entering the SAT competition 2023 A Biere, M Fleury, F Pollitt SAT COMPETITION 2023, 14, 2023 | 12 | 2023 |
| Formalization of logical calculi in Isabelle/HOL M Fleury Saarländische Universitäts-und Landesbibliothek, 2020 | 11 | 2020 |
| Scalable proof producing multi-threaded SAT solving with Gimsatul through sharing instead of copying clauses M Fleury, A Biere arXiv preprint arXiv:2207.13577, 2022 | 10 | 2022 |
Armin BiereProfessor of Computer Science, University of FreiburgVerified email at informatik.uni-freiburg.de
