Raphaël Monat

Raphaël Monat

PhD in Static Analysis

LIP6, Sorbonne Université

Welcome!

I am a permanent researcher in the SyCoMoRES team at Inria Lille. I hold a Ph.D in computer science, supervised by Antoine Miné.

The aim of my research is to improve the quality of software through the field of formal methods. I aspire to develop and apply methods to the most realistic systems possible.

These last years I focused on adding static analysis of Python programs within the ERC MOPSA project. I am also interested in the interaction between the law and the code, and I have designed a modern compiler for the French tax code, which is being transferred to the French tax administration.

My CV is available in French and in English.

News

Education

  • PhD in Computer Science, 2021 - 2019

    Sorbonne Université, France

  • Parisian Master of Research in Computer Science, 2017 - 2018

    Université Paris Diderot, France

  • Master in Fundamental Computer Science, 2015 - 2017

    École Normale Supérieure de Lyon, France

  • BSc in Fundamental Computer Science, 2014 - 2015

    École Normale Supérieure de Lyon, France

  • Classes préparatoires MPSI/MP*, option info, 2012 - 2014

    Lycée Louis-le-Grand, Paris, France

Recent Publications

Raphaël Monat (2021). Static Type and Value Analysis by Abstract Interpretation of Python Programs with Native C Libraries. PhD Thesis.

Thesis Slides YouTube Artefact

Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné (2021). A Multilanguage Static Analysis of Python Programs with Native C Extensions. SAS.

PDF DOI Approved Artefact Preprint (HAL) Slides Talk Talk (YouTube) Event

Denis Merigoux, Raphaël Monat, Jonathan Protzenko (2021). A Modern Compiler for the French Tax Code. CC.

PDF Slides Video DOI Approved Artefact Code (github) HAL Event

Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné (2020). Static Type Analysis by Abstract Interpretation of Python Programs. ECOOP.

PDF DOI Approved Artefact Slides Talk (video) Talk (YouTube) Mopsa Project Mopsa's Gitlab Event

Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné (2020). Value and Allocation Sensitivity in Static Python Analyses. SOAP.

PDF DOI Slides Talk (video) Demo (video) Talk (YouTube) Event

See all publications

Recent Talks

A Multilanguage Static Analysis of Python/C Programs with Mopsa

Mopsa is a conservative static analysis platform, independent of language and abstraction choices. Developers are free to add arbitrary abstractions (numeric, pointer, memory, etc.) and syntax iterators for new languages. Mopsa encourages the development of independent abstractions which can cooperate or be combined to improve precision.
07/07/22 Software Languages Lab, Vrije Universiteit Brussels
Slides

Formal methods for realistic systems: a study of two cases

The goal of my research is to improve the quality of software. I use for that the field of formal methods, in order to define precisely the behavior of programs. This allows to reason rigorously about these behaviors (to detect dangerous states for example).
28/04/22 LIP, ENS de Lyon
Slides

A Multilanguage Static Analysis of Python/C Programs with Mopsa

Mopsa is a conservative static analysis platform, independent of language and abstraction choices. Developers are free to add arbitrary abstractions (numeric, pointer, memory, etc.) and syntax iterators for new languages. Mopsa encourages the development of independent abstractions which can cooperate or be combined to improve precision.
17/03/22 SRG Seminar Imperial College, London
Slides

Static Type and Value Analysis by Abstract Interpretation of Python Programs with Native C Libraries

We aim at designing both theoretically and experimentally methods for the automatic detection of potential bugs in software – or the proof of the absence thereof. This detection is done statically by analyzing programs' source code without running them.
16/02/22 MTV Seminar LaBRI, Bordeaux
Slides

A Multilanguage Static Analysis of Python/C Programs with Mopsa

Mopsa is a static analyzer platform, independent of language and abstraction choices. Developers are free to add arbitrary abstractions (numeric, pointer, memory, etc.) and syntax iterators for new languages. Mopsa encourages the development of independent abstractions which can cooperate or be combined to improve precision.
31/01/22 SyCoMoRES Seminar CRIStAL, Lille
Slides
See all talks

Software

I strongly believe that academic prototypes accompanying research papers are important to show that a proposed technique works. I care about improving these prototypes to make them usable tools accessible to others, although it takes a lot of effort.

I am proud to be one of the core contributors of the following software:

Mlang

Mlang is a new compiler for M, the domain specific language used by the French Tax Administration to compute the income tax. This is joint work with Denis Merigoux.

Mopsa

Mopsa is a framework to write static analyses by abstract interpretation.

Community Service

Program Committee

  • SAS 2022

External Review Committee

  • SPLASH 2022 (round 2)

External Review

  • LOPSTR 2019
  • SOAP 2021
  • ACM TECS
  • SAS 2021

Artifact Evaluation Committee

  • SPLASH 2022 (round 2)
  • PLDI 2022
  • CAV 2022
  • ECOOP 2021
  • PLDI 2021
  • POPL 2021
  • SAS 2020

Student Volunteering

  • POPL 2017

Enseignement (en français)

2021-2022

  • LU1IN002 : éléments de programmation (C).
  • LU2IN005 : mathématiques discrètes.
  • LU2IN019 : programmation fonctionnelle (OCaml).
  • LU2IN024 : logique.
  • MU4IN500 : algorithmique avancée.
  • MU5IN554 : spécification et validation de programmes.
  • MU5IN555 : typage et analyse statique.
  • MPRI 2.6 : abstract interpretation, slides

2020-2021

  • LU3IN002 : programmation orientée objet avancée (Java).

2019-2020

  • LU1IN001 : éléments de programmation (Python).
  • MU4IN500 : algorithmique avancée.

2018-2019

Recent Posts

A Beamer snippet for remote presentations

Back in June 2020 when I was preparing my first virtual presentation, I tried leaving the top-right corner of my slides free to include a video of myself in the recordings.

Internships

Master Internship #3: Static Analysis by Abstract Interpretation: Collecting Types of Python Programs

From March to August 2018, I worked under the supervision of Antoine Miné at the LIP6 laboratory, in Paris, France. I designed a static analysis by abstract interpretation that detects potential type errors in Python programs.

Master Internship #2: Formal Verification of a Static Analyzer

From February to June 2017, I worked under the supervision of Eva Darulova at the Max Planck Institute for Software Systems (MPI-SWS), in Saarbrücken, Germany. I worked on a static analyser of floating-point programs called Daisy.

Master Internship #1: Black-box Variational Inference in Probabilistic Programs

From May to July 2016, I worked with Hongseok Yang at the University of Oxford, United Kingdom, on “Variational Inference in Probabilistic Programs”. During this internship, we expressed probabilistic programming languages into probabilistic transition systems.

Bachelor Internship: BATMAN, a BAsic Thread-Modular ANalyzer

From June to July 2015, I worked under the supervision of Antoine Miné at the École Normale Supérieure, France, on static analysis by abstract interpretation of concurrent programs. I learned how to use the Abstract Interpretation framework to develop, implement and test new methods to analyze concurrent programs more precisely.