- 2013-2016: PhD - Assisted Concurrent Program Verification by Code and Specification Transformation (Université d'Orléans)
- 2011-2013: MSc - Visualisation, Image Processing and Performances (Université d'Orléans)
- 2010-2011: BSc - Computer Sciences (Université d'Orléans)
Formal verification of critical modules of the Contiki-OS, in the context of the VESSEDIA European Project, at Inria Lille Nord Europe. The targeted OS is a lightweight IoT micro-kernel. The verification is performed using Frama-C and mainly the WP and EVA plugins.
I prepared my PhD at the Software Reliability Laboratory of the CEA List. This thesis was partially founded by the french ministry of defence. I was attached to the University of Orléans in France.
This PhD consists in the definition of a method that allows to analyze concurrent C APIs using verification tools originally meant to deal with sequential programs. It allows to transform a concurrent program and its specification to a formally equivalent sequential one.
Formal verification of a part of a concurrent paging system in an hypervisor using Frama-C and its WP plugin. This internship was at the Software Reliability Laboratory of the CEA List.
School on Formal Methods for the Design of Computer, Communication and Software Systems: Multicore Programming
(University Residential Center of Bertinoro (2015, June - 1 week))
High level models for parallel programs, weak memory models design for programming languages, garbage collectors for parallel programs.
Ecole Jeunes Chercheurs en Informatique Mathématique
(Université d'Orléans (2015, March - 1 week))
Polynomial systems resolution for real numbers, exact algorithm for NP-Hard problems, control of partially observable probabilistic models, parallel program computation in Coq, build and compute in a 2D world.
Ecole Jeunes Chercheurs en Programmation
(Inria Rennes (2014, June - 1 week))
By design correction using B, dependent types with Agda, program proof using FoCaLiZe, deductive verification of cryptographic protocols.
Program Analysis and Verification
(DigiCosme - Supélec (2013, April - 1 week))
Deductive verification (Why3), protocols verification, static analysis of numerical programs, verified programs construction using Coq.
Semantics and tools for low-level concurrent programming
(ENS Lyon (2013, January - 1 week))
Memory models (x86-TSO/ARM/Power), compiler optimizations, verification for GPUs, the C/C++11 memory model.