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, advised by Antoine Miné, during which I worked on the static analysis of Python (and Python+C) programs within the ERC MOPSA project. I have designed with Denis Merigoux a modern compiler for the French tax code, which is being transferred to the French tax administration.

The aim of my research is to improve the quality of software through the field of formal methods, and mainly automated program verification. I aspire to develop and apply methods to the most realistic systems possible. I have a particular interest in implementations of computational laws (taxes, benefits).

These days, I am exploring

  • ways to facilitate the adoption of static analysis tools,
  • developing formal methods tools for Catala, a domain-specific language for the implementation of legislative texts. This is a joint research project with Aymeric Fromherz.
  • static analysis of binary code following previous works of my team.

I am also one of the maintainers of the Mopsa static analyzer.

I am looking for motivated interns (sample topic), PhD students, postdocs & collaborators. Informal inquiries are welcome, feel free to send me an email!

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.

Recent Publications

Pierre Goutagny, Aymeric Fromherz, Raphaël Monat (2025). CUTECat: Concolic Execution for Computational Law. ESOP.

Preprint

Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné (2024). Easing Maintenance of Academic Static Analyzers. CSV 2024 STTT special issue.

PDF arXiv HAL

Raphaël Monat, Marco Milanese, Francesco Parolini, Jérôme Boillot, Abdelraouf Ouadjaout, Antoine Miné (2024). Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution). TACAS.

PDF SV-Comp results Slides Editor HAL

Raphaël Monat, Aymeric Fromherz, Denis Merigoux (2024). Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law. ESOP. SCP award for the ETAPS best tool paper.

PDF Artefact (reviewed A,F,R) Slides HAL Editor Award

Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné (2023). Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution). TACAS.

PDF DOI Validated Artefact HAL Slides SV-Comp results

See all publications

Recent Talks

Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law
14/11/24 Irif, Paris
An Overview of Automated Program Analysis
21/10/24 Lille
Easing implementation and maintenance of academic static analyzers
20/09/24 Paris
Mopsa tutorial
04/09/24 Lipari, Italy
Easing implementation and maintenance of academic static analyzers
06/06/24 Venice, Italy
See all talks

Students

Current students

Past students

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

  • NSAD 2024
  • DEBT 2024
  • SOAP 2024 (chair and invited editor for STTT special issue with Cindy Rubio González)
  • JFLA 2024
  • SOAP 2023
  • SV-Comp 2023
  • SAS 2022

External Review Committee

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

External Review

  • JLAMP 2024 (x 2)
  • STTT 2024
  • Journal of Systems & Software 2024
  • ATVA 2023
  • Science of Computer Programming
  • LOPSTR 2019
  • SOAP 2021
  • ACM TECS
  • SAS 2021

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.

Funded Projects

ANR-JCJC RAISIN: Resource-Aware conservatIve StatIc aNalysis
Inria-AEx AVoCAT: Automated Verification of Catala programs

Visibility

Enseignement (en français)

2023-2024

  • Compilation, M1 Université de Lille.

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

Recent Posts

Notes on applying to CS faculty positions in France

These are a few notes regarding the application to CS faculty positions in France, based on my experience applying during the academic year 2021–2022. Please note: this is still valid in 2024 but may get outdated later on, this concerns early-career positions, there are also full professor or research director positions.

My current approach to low-carbon research

I have signed the TCS4F pledge for sustainable research in (theoretical) computer science. Below are some specific actions I am taking. Flight-free business travel In particular, I have not taken a plane to attend conferences since Fall 2019.

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.

Contact