Version française

Lionel Rieg

Since September 2018, I am a Maître de Conférence (assistant lecturer) at the Verimag laboratory (Synchrone team) and at the Ensimag/Grenoble-INP.

Previously, I have been:


My list of publications.

Real-time CertiKOS

This project aims at adding real-time properties to CertiKOS, a verified muticore OS kernel.
To this end, we extend CertiKOS with required features: RDTSC support, preemptive interrupts, preemptive priority-based scheduling, etc. We also revisit classical results of real time scheduling theory through a formal proof perspective and using the abstractions already provided by CertiKOS (layers) which combines into the concept of virtual time.

Formal Proofs in Distributed Computing

About Robot Swarms

The Pactole project aims at formalizing results about robot swarms in a unified framework. This framework supports both impossibility proofs (for instance, impossibility of gathering on a real line) and proofs of algorithms (for instance, gathering in the plane).

In Autostabilizing Algorithms

The Estate project formally certifies the correctness of auto-stabilizing algorithms, building upon the Coq development PADEC.

Formal Proofs about the Compilation of Synchronous Languages

PhD Work

My PhD thesis.

How to Contact Me