Raphaël Monat

Research Scientist (he/him)

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. The techniques and analysis are mostly developed within the Mopsa analysis platform, which I co-maintain.
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.
open science and reproducibility of software-generated experimental data. I am a member of the “Source code and software” subgroup from the French Committee for Open Science. With colleagues, we wrote “CODE beyond FAIR”, with a shorter version available as a Nature Commentary.

I am looking for motivated interns, PhD students, postdocs & collaborators. Applicants from all backgrounds, horizons, genders and ages are encouraged to apply. Informal inquiries are welcome, do feel free to send me an email!

News

Happy to announce a public release of Try-Mopsa, you can read more about it in a preprint.
Looking forward to co-chair the Artifact Evaluation of PLDI 2026.
I have been granted an Amazon Research Award!.
Consider joining the Abstract Interpretation Zulip and the Mopsa Zulip for discussions.

I attended a Dagstuhl Seminar on “Sound Static Program Analysis in Modern Software Engineering” and another Dagstuhl Seminar on “Testing Program Analyzers and Verifiers”.

"Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law" has been accepted at ESOP'24. Delighted to announce that this work has been awarded the ETAPS best tool paper!

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

Raphaël Monat (2025). Try-Mopsa: Relational Static Analysis in Your Pocket. Preprint.

PDF Try-Mopsa HAL arXiv

Raphaël Monat, Liane Huttner (2025). Coding computational laws: 20 recommendations for public administrations. Preprint.

PDF HAL

Milla Valnet, Raphaël Monat, Antoine Miné (2025). Compositional Static Value Analysis for Higher-Order Numerical Programs. ECOOP.

HAL Editor Artefact (reviewed A,F,R)

Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné (2025). Mopsa-C with Trace Partitioning and Autosuggestions (Competition Contribution). TACAS.

PDF SV-Comp results HAL Editor

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

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

See all publications

Recent Talks

Try-Mopsa: Relational Static Analysis in Your Pocket

16/10/25 Schloss Dagstuhl

Formal methods for public administrations

19/06/25 Lille

The Mopsa static analysis platform, and our quest to ease implementation & maintenance

11/06/25 Schloss Dagstuhl

Mopsa at the Software-Verification Competition

02/06/25 Lille

The Mopsa static analysis platform, and our quest to ease implementation & maintenance

04/04/25 Online (Colorado Boulder)

See all talks

Students

Current students

Milla Valnet, PhD student (since Sep. 2023), co-advised by Antoine Miné.
Pierre Goutagny, PhD student (since Sep. 2024), co-advised by Aymeric Fromherz and Patrick Baillot.
Tom Goalard, M1 intern (Sep. – Dec. 2025), co-advised by Julien Forget.
Leonardo Speranzon, PhD student (starting Oct. 2025), co-advised by Julien Forget.

Past students

Aymane Ismail, M2 project (Jan. – Feb. 2025).
Pierre Goutagny, M2 intern (Oct. 2023 – March 2024), co-advised by Aymeric Fromherz.
Andrei Florea, PhD student (Sep. 2022 – Sep. 2023), co-advised by Julien Forget and Clément Ballabriga.
Milla Valnet, M2 intern (March – July 2022), co-advised by Antoine Miné.

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

Chairing

PLDI 2026 Artifact Evaluation chair with Qirun Zhang.
ECOOP 2025 Artifact Evaluation chair with Karine Even-Mendoza and Yannick Zakowski
ECOOP 2024 Artifact Evaluation chair with Karine Even-Mendoza
Invited editor for STTT special issue with Cindy Rubio González
SOAP 2024 (workshop) PC chair with Cindy Rubio González

Program Committee (international conferences)

Program Committee (workshops, national conferences, and competitions)

Extended Review Committee

External Review

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

Artifact Evaluation Committee

Scientific expertise

External ANR reviewer in 2023

Others

Part of the benchmark quality assurance team of SV-Comp, in charge of maintaining the repository and the quality of more than 30,000 C programs used in the competition and by the community to evaluate new analyses.
POPL 2017 Student Volunteer

Some specific French duties

Niveau national

Jury concours 2025 CRCN/ISFP Inria Lille, co-référent parité égalité des chances. Le concours a reçu 31 candidatures et auditionné 13 personnes sur deux jours.
Membre du CSI de Dorian Lesbre.
J’ai été jury en Juin 2023 et en Juin 2024 des oraux d’informatique, sur les concours d’entrées aux Écoles Normales Supérieures via les filières MP et MPI des classes préparatoires. Les rapport du jury sont disponibles (2023, 2024)

Depuis Mars 2022, je suis membre du “collège logiciel” du Comité National pour la Science Ouverte.

Niveau local

Co-organisation avec Clémentine Maurice, d’une visite des laboratoires CRIStAL et Inria pour les étudiant.e.s de L3 et M1 de l’ENS Rennes (janvier 2025). Cette visite sur 3 jours a permis à 44 étudiant.e.s d’interagir avec une bonne quarantaine de collègues (postdoc, ingénieurs de recherche, C et E/C), rattachés à CRIStAL, Inria et l’IRCICA.
Je participe à la commission parité et égalité femmes-hommes du laboratoire CRIStAL depuis janvier 2023.
- Co-organisation de séminaires “100% parité”. Un des séminaires a notamment permis de créer des ressources sur le bien-être au travail.
- Participation à la création de fiches sur l’aide institutionnelle dans les situations de harcèlement, de discrimination ou de conflit.
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

Amazon Research Awards: Resource-Aware Conservative Static Analysis

ANR-JCJC RAISIN: Resource-Aware conservatIve StatIc aNalysis

Inria-AEx AVoCAT: Automated Verification of Catala programs

Visibility

Invited to Dagstuhl Seminar on “Sound Static Program Analysis in Modern Software Engineering”.
Invited to Dagstuhl Seminar on “Testing Program Analyzers and Verifiers”.
ETAPS 2025 distinguished artifact for “CUTECat: Concolic Execution for Computational Law”.
SV-Comp 2025 Silver Medal in the “Software Systems” category.
Amazon Research Award, Fall 2024 (cf. funding).
Lecturer at the Lipari 2024 Summer School on Abstract Interpretation.
ETAPS 2024 best tool paper award for “Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law”.
Invited speaker at the ETAPS 2024 Mentoring Workshop.
SV-Comp 2024 Gold Medal in the “Software Systems” category.
SV-Comp 2023 Bronze Medal in the “Software Systems” category.
ECOOP 2023 Distinguished Artifact Reviewer Award.
Invited to Dagstuhl Seminar 23281.
SOAP 2020 Best Presentation Award for “Value and Allocation Sensitivity in Static Python Analyses”.

Enseignement (en français)

2024-2025

Compilation, M1 Université de Lille

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.
- Correction interrogation de TD.
LU2IN019 : programmation fonctionnelle (OCaml).
LU2IN024 : logique.
MU4IN500 : algorithmique avancée.
MU5IN554 : spécification et validation de programmes.
- TME 1
- TME 2 (squelette)
- TME 3
- TME 4 (squelette)
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

1I001 : éléments de programmation (Python).
- Correction TME solo
ARE Calrais : atelier de recherche encadré sur le calcul et le raisonnement.
2I008 : programmation fonctionnelle en OCaml
3I018 : compilation.