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:
NEW: Internship opportunities for 2020!
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 leads us to define the concept of virtual timelines.
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,
gathering on a real line) and proofs of algorithms
(for instance, gathering in the
In Autostabilizing Algorithms
project formally certifies the correctness of auto-stabilizing
algorithms, building upon the Coq
Formal Proofs about the Compilation of Synchronous Languages
My PhD thesis.
My list of publications.
How to Contact Me
- by e-mail: email@example.com