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.
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,
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
- Formalizing the compilation of Esterel towards digital
circuits, the final objective being to extract a proven compiler, in the
style of CompCert;
- Formalization of the compilation of Lustre towards
imperative code, in particular towards CompCert intermediate
My PhD thesis.
How to Contact Me
- by e-mail: firstname.lastname@example.org