Follow
Leon Gondelman
Leon Gondelman
Post-doctoral researcher, Aarhus University, Denmark
Verified email at cs.au.dk - 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 (3), 152-174, 2016
762016
A pragmatic type system for deductive verification
JC Filliâtre, L Gondelman, A Paskevich
222016
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
172018
The matrix reproved (verification pearl)
M Clochard, L Gondelman, M Pereira
Journal of Automated Reasoning 60 (3), 365-383, 2018
112018
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
82021
Semi-automated Reasoning About Non-determinism in C Expressions.
D Frumin, L Gondelman, R Krebbers
ESOP, 60-87, 2019
72019
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, 2021
62021
The matrix reproved (verification pearl)
M Clochard, L Gondelman, M Pereira
Working Conference on Verified Software: Theories, Tools, and Experiments …, 2016
52016
Double WP: Vers une preuve automatique d'un compilateur
M Clochard, L Gondelman
Journées Francophones des Langages Applicatifs, 2015
32015
A toolchain to produce verified OCaml libraries
JC Filliâtre, L Gondelman, C Lourenço, A Paskevich, M Pereira, ...
22020
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
12022
A benchmark for C program verification
M van Eekelen, D Frumin, H Geuvers, L Gondelman, R Krebbers, ...
arXiv preprint arXiv:1904.01009, 2019
12019
Semi-Automated Reasoning About Non-Determinism in C Expressions
L Gondelman
2019
Un système de types pragmatique pour la vérification déductive des programmes
L Gondelman
Université Paris Saclay (COmUE), 2016
2016
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols
L GONDELMAN, JK HINRICHSEN, M PEREIRA, A TIMANY, L BIRKEDAL
A Toolchain for Verified OCaml Programs
JC Filliâtre, L Gondelman, A Paskevich, M Pereira
The system can't perform the operation now. Try again later.
Articles 1–16