| The spirit of ghost code JC Filliâtre, L Gondelman, A Paskevich Formal Methods in System Design 48, 152-174, 2016 | 110 | 2016 |
| Finite sets in homotopy type theory D Frumin, H Geuvers, L Gondelman, N Weide Proceedings of the 7th ACM SIGPLAN International Conference on Certified …, 2018 | 32 | 2018 |
| A pragmatic type system for deductive verification JC Filliâtre, L Gondelman, A Paskevich | 25 | 2016 |
| Distributed causal memory: modular specification and verification in higher-order distributed separation logic L Gondelman, SO Gregersen, A Nieto, A Timany, L Birkedal Proceedings of the ACM on Programming Languages 5 (POPL), 1-29, 2021 | 23 | 2021 |
| Verifying reliable network components in a distributed separation logic with dependent separation protocols L Gondelman, JK Hinrichsen, M Pereira, A Timany, L Birkedal Proceedings of the ACM on Programming Languages 7 (ICFP), 847-877, 2023 | 17 | 2023 |
| Modular verification of op-based CRDTs in separation logic A Nieto, L Gondelman, A Reynaud, A Timany, L Birkedal Proceedings of the ACM on Programming Languages 6 (OOPSLA2), 1788-1816, 2022 | 16 | 2022 |
| Trillium: Unifying refinement and higher-order distributed separation logic A Timany, SO Gregersen, L Stefanesco, L Gondelman, A Nieto, L Birkedal | 13 | 2022 |
| Semi-automated Reasoning About Non-determinism in C Expressions. D Frumin, L Gondelman, R Krebbers ESOP, 60-87, 2019 | 13 | 2019 |
| The matrix reproved (verification pearl) M Clochard, L Gondelman, M Pereira Journal of Automated Reasoning 60, 365-383, 2018 | 11 | 2018 |
| Trillium: higher-order concurrent and distributed separation logic for intensional refinement A Timany, SO Gregersen, L Stefanesco, JK Hinrichsen, L Gondelman, ... Proceedings of the ACM on Programming Languages 8 (POPL), 241-272, 2024 | 8 | 2024 |
| A Pragmatic Type System for Deductive Software Verification L Gondelman < bound method Organization. get_name_with_acronym of< Organization: TEL …, 2016 | 4 | 2016 |
| Double WP: Vers une preuve automatique d'un compilateur M Clochard, L Gondelman Journées Francophones des Langages Applicatifs, 2015 | 4 | 2015 |
| A toolchain to produce verified OCaml libraries JC Filliâtre, L Gondelman, C Lourenço, A Paskevich, M Pereira, ... | 3 | 2020 |
| The matrix reproved (verification pearl) M Clochard, L Gondelman, M Pereira Verified Software. Theories, Tools, and Experiments: 8th International …, 2016 | 3 | 2016 |
| A benchmark for C program verification M van Eekelen, D Frumin, H Geuvers, L Gondelman, R Krebbers, ... arXiv preprint arXiv:1904.01009, 2019 | 2 | 2019 |
| A Toolchain to Produce Correct-by-Construction OCaml Programs JC FilliÂtRe, L Gondelman, A Paskevich, M Pereira, SM de Sousa Rapp. tech. artifact: https://www. lri. fr/~ mpereira/correct_ocaml. ova, 2018 | 2 | 2018 |
| Modular Verification of State-Based CRDTs in Separation Logic A Nieto, A Daby-Seesaram, L Gondelman, A Timany, L Birkedal 37th European Conference on Object-Oriented Programming (ECOOP 2023), 2023 | 1 | 2023 |
| Reasoning about Weak Isolation Levels in Separation Logic AA Mathiasen, L Gondelman, L Ducruet, A Timany, L Birkedal arXiv preprint arXiv:2501.14421, 2025 | | 2025 |
| Modular Verification of State-Based CRDTs in Separation Logic AN Rodriguez, A Daby-Seesaram, L Gondelman, A Timany, L Birkedal Leibniz International Proceedings in Informatics (LIPIcs), 2023 | | 2023 |
| Semi-Automated Reasoning About Non-Determinism in C Expressions L Gondelman | | 2019 |
