Léon Gondelman's Home Page
I am a post-doc researcher at Aarhus Univeristy, Denmark, at Logic and Semantics Group. I am interested in modular specification and verification of distributed systems. I am currently working on reasoning about distributed causal memory and partition-tolerant distributed storage systems.
Previously, I was a post-doc at iCIS in Nijmegen, Netherlands, where I was a member of Sovereign project, developping methods and tools for the verification of life-critical or safety-critical systems. I was working there on formalization of C language in Coq proof assistant using a higher-order concurrent separation logic framework called Iris. On top of Iris, we had built a program logic that comes with a semi-automated reasoning about non-determinism in C expressions.
Before my post-doc, I defended my PhD in December 2016 under supervision of Jean-Christophe Filliâtre and Andrei Paskevich at Université Paris Saclay in France. My PhD thesis entitled "A Pragmatic Type System for Deductive Verification" explores solutions that a type system based approach can bring to the deductive verification. It formalizes some aspects of the type system of Why3 such as ghost code and static control of aliases.
- lists of my publications
- main research topics :
- verification of fault-tolerant distributed systems
- program logics, deductive software verification
- functional programming
- type systems and static analysis
- design and development of software in educuation
- I was teaching assistant for the course on Iris at Aarhus University in 2019 and 2020.
- I was teaching assistant for the course on finite automata at Radboud University during my post-doc at Radbouad (2017-2018).
- During three years of my PhD (2013-2016), I was a teaching assistant for bachelor and master courses of functional programming, compilation, and logics.