International Conference Papers

[c6] Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, Lars Birkedal. Modular Verification of State-Based CRDTs in Separation Logic., in ECOOP, 2023. [DOI]
[c5] Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, and Lars Birkedal. Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic. Principles of Programming Languages (POPL), 2021. [ .pdf ]
[c4] Dan Frumin, Léon Gondelman, and Robbert Krebbers. Semi-automated reasoning about non-determinism in C expressions. European Symposium on Programming (ESOP), 2019. [ .pdf ]
[c3] Dan Frumin, Léon Gondelman, Herman Geuvers, and Niels van der Weide. Finite Sets in Homotopy Type Theory. Certified Programs and Proofs (CPP), 2018. [ .pdf ]
[c2] Martin Clochard, Léon Gondelman, and Mário Pereira. The Matrix reproved. In Sandrine Blazy and Marsha Chechik, editors, 8th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Lecture Notes in Computer Science, Toronto, Canada, July 2016. Springer. [ bib | full text on HAL ]
[c1] Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. The spirit of ghost code. In Armin Biere and Roderick Bloem, editors, 26th International Conference on Computer Aided Verification, volume 8859 of Lecture Notes in Computer Science, pages 1--16, Vienna, Austria, July 2014. Springer. [ bib | full text on HAL | .pdf ]

Journal Papers

[j6] Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, and Lars Birkedal. Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement, POPL, 2024. [DOI]
[j5] Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, and Lars Birkedal. Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols, ICFP, 2023. [DOI]
[j4] Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, and Lars Birkedal. Modular Verification of Op-Based CRDTs in Separation Logic, in OOPSLA2 (POPL), 2022. [DOI]
[j3] Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, and Lars Birkedal. Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic, in Principles of Programming Languages (POPL), 2021. [DOI]
[j2] Martin Clochard, Léon Gondelman, and Mário Pereira. The Matrix Reproved (Verification Pearl). Journal of Automated Reasoning, October, 2017. [ DOI | .pdf ]
[j1] Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. The spirit of ghost code. Formal Methods in System Design, 48(3):152--174, 2016. [ bib | DOI | full text on HAL ]

National Conference Papers

[n1] Martin Clochard and Léon Gondelman. Double WP: vers une preuve automatique d'un compilateur. In Vingt-sixièmes Journées Francophones des Langages Applicatifs, Val d'Ajol, France, January 2015. [ bib | full text on HAL ]

Unpublished

[s1] Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich, and Mário Pereira. A Toolchain for Verified OCaml Programs. [ .pdf ]

Technical Reports

[r2] Léon Gondelman. Un système de types pragmatique pour la vérification déductive des programmes. PhD Thesis, Université Paris Sud, December 2016. [ .pdf ]
[r1] Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. A pragmatic type system for deductive verification. Research report, Université Paris Sud, 2016. [ bib | full text on HAL ]