Education

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

Research Activity

Post-doctoral research

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.

Doctoral research

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.

MSc internship

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.

Schools

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.