I am a PhD student under the supervision of Jérôme Feret in the Antique team at the ENS. I'm working to improve the Astrée static analyzer to be able to prove some security properties of an operating system. This implies to find ways to make the memory models of C and assembly to work together. Moreover, we need to be able to handle ghost variables to express complex properties inherent to low-level source code.

News

  • I am a member of the SAS 2020 Artifact Evaluation Committee

Interests

  • Static Program Analysis
  • Abstract Interpretation
  • Computability Theory

Education

  • MSc in Computer Science, 2016

    École Normale Supérieure de Lyon/EPFL

  • BSc in Computer Science, 2014

    École Normale Supérieure de Lyon

Projects

AstréeS

Astrée for Security

Talks

Program Verification by Abstract Interpretation

A quick introduction to abstract interpretation

Sharing Ghost Variables in a Collection of Abstract Domains

Publications

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 …

Software

OColor

OCaml Print with style in your terminal using Format's semantic tags

Epictetus

OCaml Print aligned tables with mixed column sub-division

Plato

OCaml Python standard library in OCaml

Socrates

Python Testing tool

Student

Former intern

Contact

  • marc.chevalier@ens.psl.eu
  • Antique - Département d'informatique
    École Normale Supérieure
    45, rue d'Ulm
    F-75230 Paris CEDEX 05, France