Léon Gondelman's Home Page

 

About:

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.

News:

08/04/2019	-	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)
08/01/2019	-	Check out AutoMate tool I have recently developped !

Research:

• 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

Software

Teaching:

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