Expert en analyse statique

École Normale Supérieure

J’ai récemment soutenu ma thèse, sous la supervision de Jérôme Feret, dans l’équipe Antique à l’ENS. Je travaille à l’amélioration de l’analyseur statique Astrée pour prouver des propriétés de sécurités d’un système d’exploitation. Cela demande de faire travailler ensemble les modèles mémoire de l’assembleur et du C. De plus, Astrée doit être capable de gérer des variables fantômes pour exprimer des propriétés complexes inhérentes à la programmation bas niveau.

News

  • April 2023: Je suis chair du comité d’évaluation des artefacts de SAS 2023.
  • April 2022: Je suis chair du comité d’évaluation des artefacts de SAS 2022.
  • Novembre 2020: J’ai soutenu. Voyez plus sur ma soutenance.
  • Avril 2020: Je fais partie du comité d’évaluation des artefacts de SAS 2020.

Intérêts

  • Analyse statique
  • Interpretation abstraite
  • Méthodes formelles
  • Languages de programmation
  • Compilateurs
  • Systèmes embarqués
  • Systèmes d’exploitation
  • CPU architecture

Formation

  • Doctorat en informatique, 2020

    École Normale Supérieure

  • Master en informatique, 2016

    École Normale Supérieure de Lyon/EPFL

  • Licence en informatique, 2014

    École Normale Supérieure de Lyon

Projets

AstréeS

Astrée pour la Securité

Talks

Proving the Security of Software-Intensive Embedded Systems by Abstract Interpretation

Ma soutenance de thèse
Friday, November 27, 2020 14:00 — 17:00 🇫🇷 ENS, France
Diapositives Manuscrit PV du jury

Vérification de programmes par interprétation abstraite

Rapide introduction à l’interprétation abstraite
Monday, September 14, 2020 10:20 — 10:40 🇫🇷 ENS, France
Diapositives
Plus de présentations

Publications

Analyse de la sécurité de systèmes critiques embarqués à forte composante logicielle par interprétation abstraite

Cette thèse est consacrée à l’analyse de logiciels de bas niveau, tels que les systèmes d’exploitation, par interprétation …
Marc Chevalier
PDF Projet Diapositives

Sharing Ghost Variables in a Collection of Abstract Domains

We propose a framework in which we share ghost variables across a collection of abstract domains allowing precise proofs of complex …
Marc Chevalier, Jérôme Feret
PDF Projet Diapositives DOI Springer

Enseigne­ment

Mathematiques, L1, LFDV, CRI

Semantics and applications to verification, L3, ENS

Software

OColor

OCaml Afficher avec style dans votre terminal en utilisant les tags sémantiques de Format

Epictetus

OCaml Afficher des tableaux bien alignés malgré une hiérarchie changeante de sous-colonnes

Plato

OCaml Librarie standard de Python en OCaml

Socrates

Python Outil de test

Étudiant

Ancien stagiaire

Contact