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.

High level models for parallel programs, weak memory models design for programming languages, garbage collectors for parallel programs.

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.

By design correction using B, dependent types with Agda, program proof using FoCaLiZe, deductive verification of cryptographic protocols.

Deductive verification (Why3), protocols verification, static analysis of numerical programs, verified programs construction using Coq.

Memory models (x86-TSO/ARM/Power), compiler optimizations, verification for GPUs, the C/C++11 memory model.