Léon Gondelman's Home Page



I am a post-doc researcher at iCIS in Nijmegen, Netherlands. I am member of Sovereign project, developping methods and tools for the verification of life-critical or safety-critical systems.

Currently, I am working on formalization of C language in Coq proof assistant using a higher-order concurrent separation logic framework called Iris. On top of Iris, we have recently 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.


Our paper "Semi-automated reasoning about non-determinism in C expressions" with Dan Frumin and Robbert Krebbers has been accepted to ESOP conference. (website, paper, slides)
Check out AutoMate tool I have recently developped !


  • lists of my publications

  • main research topics :
    • program logics, deductive software verification
    • functional programming
    • type systems and static analysis
    • design and development of software in educuation
    • homotopy type theory, higher inductive types


I am developping AutoMate, a tool that assists students and tutors in teaching course on formal languages.

The goal is twofold to help:

  • students to solve exercises by checking whether their answers are correct and giving them a detailed feedback.
  • tutors to prepare assignments in an efficient way, by extracting description and automated grading procedure directly from latex sources.


  • I am teaching assistant for the course on finite automata at Radboud University for this year and the previous year.
  • During three years of my PhD, I was a teaching assistant for bachelor and master courses of functional programming, compilation, and logics.

Contact information:

  • Email: leon dot gondelman at gmail dot com
  • Office: 01.03, Mercator 1 building, Toernooiveld 212, Nijmegen 6525 EC