Raphaël Monat

Raphaël Monat

Research Scientist

Inria & University of Lille

I am a research scientist 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.

I previously worked on the static analysis of Python and C programs within the ERC MOPSA project. I am one of the maintainers of the Mopsa static analyzer. I am also interested in the interaction between the law and the code, and I have designed with Denis Merigoux a modern compiler for the French tax code, which is being transferred to the French tax administration.

These days, I am exploring ways to facilitate the adoption of static analysis tools; static analysis of binary code following previous works of my team; and the ongoing application of formal methods to Catala, a domain-specific language for the implementation of legislative texts.

My CV is available in French and in English.

Feel free to send me an email if you are interested in working with me!

News

Previous Research Experiences

  • Static Type and Value Analysis by Abstract Interpretation of Python Programs with Native C Libraries.
    Under the supervision of Antoine Miné - 2018 -- 2021.

    APR team, LIP6, Sorbonne Université, Paris, France.

  • Formal verification of Static Analyses of Floating-point Programs.
    Under the supervision of Eva Darulova - February to June 2017.

    Automated Verification and Approximation team, MPI-SWS, Saarbrücken, Germany.

  • Black-box Variational Inference in Probabilistic Programming.
    Under the supervision of Hongseok Yang - May to July 2016.

    Department of Computer Science, University of Oxford, UK.

  • Abstract Interpretation of Concurrent Programs.
    Under the supervision of Antoine Miné - June & July 2015.

    ANTIQUE Team, École Normale Supérieure, Paris, France.

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:

Mopsa

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

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.

Community Service

Program Committee

External Review Committee

  • ECOOP 2023 (rounds 1 & 2)
  • SPLASH 2023 (rounds 1 & 2)
  • SPLASH 2022 (round 2)

External Review

  • LOPSTR 2019
  • SOAP 2021
  • ACM TECS
  • SAS 2021
  • Science of Computer Programming
  • ATVA 2023

Artifact Evaluation Committee

  • ECOOP 2024 (chair with Karine Even-Mendoza)
  • ECOOP 2023 (rounds 1 & 2)
  • SPLASH 2023 (rounds 1 & 2)
  • SPLASH 2022 (round 2)
  • PLDI 2022
  • CAV 2022
  • ECOOP 2021
  • PLDI 2021
  • POPL 2021
  • SAS 2020

Student Volunteering

  • POPL 2017

Scientific expertise

  • External ANR reviewer in 2023

Some specific French duties

Niveau national

Niveau local

  • Je participe à la commission parité et égalité femmes-hommes du laboratoire CRIStAL depuis janvier 2023.
  • Je suis membre suppléant de la FSS de l’Inria Lille (Formation Spécialisée de Site, ex CLHSCT), depuis janvier 2023.

Students

Current students

  • Milla Valnet, PhD student (since Sep. 2023), co-advised by Antoine Miné.
  • Pierre Goutagny, M2 intern (Oct. 2023 – March 2024), co-advised by Aymeric Fromherz.

Past students

Enseignement (en français)

2022-2023

  • Compilation, M1 Université de Lille.

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

Contact