Follow
Leon Gondelman
Leon Gondelman
Assistant Professor, Aalborg University @ Copenhagen, Denmark
No verified email - Homepage
Title
Cited by
Cited by
Year
The spirit of ghost code
JC Filliātre, L Gondelman, A Paskevich
Formal Methods in System Design 48, 152-174, 2016
972016
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
272018
A pragmatic type system for deductive verification
JC Filliātre, L Gondelman, A Paskevich
232016
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
222021
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
132022
Trillium: Unifying refinement and higher-order distributed separation logic
A Timany, SO Gregersen, L Stefanesco, L Gondelman, A Nieto, L Birkedal
arXiv preprint arXiv:2109.07863, 27, 2021
132021
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
112023
The matrix reproved (verification pearl)
M Clochard, L Gondelman, M Pereira
Journal of Automated Reasoning 60, 365-383, 2018
112018
Semi-automated Reasoning About Non-determinism in C Expressions.
D Frumin, L Gondelman, R Krebbers
ESOP, 60-87, 2019
102019
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
52024
The matrix reproved (verification pearl)
M Clochard, L Gondelman, M Pereira
Verified Software. Theories, Tools, and Experiments: 8th International …, 2016
52016
Double WP: Vers une preuve automatique d'un compilateur
M Clochard, L Gondelman
Journées Francophones des Langages Applicatifs, 2015
42015
A toolchain to produce verified OCaml libraries
JC Filliātre, L Gondelman, C Lourenēo, A Paskevich, M Pereira, ...
32020
A Pragmatic Type System for Deductive Software Verification
L Gondelman
PhD thesis, Université Paris-Saclay, 2016
32016
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
22018
A benchmark for C program verification
M van Eekelen, D Frumin, H Geuvers, L Gondelman, R Krebbers, ...
arXiv preprint arXiv:1904.01009, 2019
12019
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
Modular Verification of State-Based CRDTs in Separation Logic (Artifact)
A Nieto, A Daby-Seesaram, L Gondelman, A Timany, L Birkedal
Schloss-Dagstuhl-Leibniz Zentrum für Informatik, 2023
2023
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
2023
Semi-Automated Reasoning About Non-Determinism in C Expressions
L Gondelman
2019
The system can't perform the operation now. Try again later.
Articles 1–20