Léon; Gondelman's Home Page

 

About:

About:

I am an assistant professor at Aalborg University @ Copenhagen at DEIS - Distributed, Embedded and Intelligent Systems. I am interested in modular specification and verification of distributed systems. I am currently working on reasoning about distributed transactions and partition-tolerant distributed storage systems.

Previously, I was a post-doc researcher at Aarhus Univeristy, Denmark, at Logic and Semantics Group and before that 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 and link to DBLP profile

  • 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 (Lecturer):

Teaching (Teaching Assistant):

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