About me

I am currently a researcher and deputy head of lab at the Software Reliability and Security Laboratory of the CEA LIST. Previously, I was a post-doc researcher at Inria Nord Europe for the EU H2020 VESSEDIA project. Before that, I was a teaching and research assistant (ATER) at the university institute of technology of Orléans, associated to the Laboratoire d'Informatique Fondamentale d'Orléans (LIFO). I prepared my PhD at the Software Reliability and Security Laboratory of the CEA LIST.

I am interested in the analysis of concurrent code using formal methods and more precisely proof.

Research

Currently, I am involved in the development of Frama-C, a platform for the analysis of C programs, using different plugins that provides different kind of analyses and allows to get different levels of confidence into the analyzed software. I mainly work on the deductive verification plug-in of Frama-C which allows verifying that a program conforms to its specification.

Previously, I worked for the EU H2020 VESSEDIA project that aims at making formal methods easier to apply in the context of the internet-of-things where many security risks are rising as IoT devices are more and more widespread. My current work is to apply formal verification to the Contiki microkernel (an lightweight OS for IoT) and its libraries, mostly to show the absence of runtime errors. I mostly use Frama-C with the EVA plugin and the WP plugin.

In the context of Contiki, concurrency is only simulated using a library called protothread which allows cooperative multi-tasking without the need of multiple stacks.

My PhD thesis work is about a (formally correct) code and specification transformation from concurrent to equivalent sequential code. It allows one to verify a concurrent code using tools dedicated to sequential code. Such a transformation is valid under the assumption that the verified program has a sequentially consistent behavior. Our processors implements memory models that do not guarantee it. A part of my work is to study these models, and to define ways to analyze programs taking them in account.

Events

Past:

  • 10/2019 - FM 2019, Porto, Portugal (Tutorial)
  • 07/2019 - Program Committee: 4PAD 2019, Dublin, Ireland
  • 04/2019 - SAC 2019, Limassol, Cyprus (Paper slides + Tutorial slides)
  • 01/2018 - FIC 2019, Lille, France slides
  • 07/2018 - Program Committee: 4PAD 2018, Orléans, France
  • 07/2018 - Tutorial: HPCS 2018, Orléans, France slides
  • 06/2018 - Talk: TAP 2018, Toulouse, France slides
  • 06/2018 - Talk: AFADL 2018, Grenoble, France slides
  • 05/2018 - Tutorial: ZINC 2018, Novi Sad, Serbia slides
  • 04/2018 - Talk: NFM 2018, Newport News, VA, USA slides
  • 06/2017 - Talk: AFADL 2017, Montpellier, France slides
  • 12/2016 - PhD Thesis Defence, Saclay, France slides
  • 07/2016 - Talk: CSTVA 2016, Saarbrücken, Germany slides
  • 06/2016 - Frama-C Day 2016, Paris, France slides
  • 06/2015 - Talk: FMICS 2015, Oslo, Norway slides
  • 06/2015 - Talk: AFADL 2015, Bordeaux, France slides
  • 03/2015 - EJC IM 2015, Orléans, France
  • 12/2014 - Forum STIC 2014, Saclay, France slides
  • 06/2014 : EJCP 2014, Rennes, France

Teaching

I am the author of a tutorial on Frama-C and WP.

I mainly teach code validation (using test and deductive proof), algorithms (basics, and then graphs and automaton), methods and languages for object-oriented design, and multi-core programmings (parallelism and concurrency).