Léon Gondelman's Home Page

 

About:

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.

Research:

• 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

Teaching:

• 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.