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.
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, PhD students, postdocs & collaborators. Informal inquiries are welcome, feel free to send me an email!

News

I have been awarded an ANR Young Researcher Grant to pursue Resource-Aware Conservative Static Analysis (RAISIN), starting Fall 2024!
Looking forward to giving a tutorial at the Lipari Summer School on Abstract Interpretation.
"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!
For our second participation, Mopsa won the gold medal by a long shot in the SoftwareSystems category of SV-Comp. In our first participation, we earned the bronze medal. See more details in our short TACAS paper.
Gave an invited talk at ETAPS' mentoring workshop.
Chairing SOAP@PLDI'24 program committee with Cindy Rubio González.
Chairing ECOOP'24 artifact evaluation committee with Karine Even-Mendoza.
I am honored to have received a Distinguished Artifact Reviewer Award at ECOOP'23.
I was invited to the Dagstuhl Seminar on Theoretical Advances and Emerging Applications in Abstract Interpretation.
I am a member of the “Source code and software” subgroup from the French Committee for Open Science.

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, Abdelraouf Ouadjaout, Antoine Miné (2024). Easing Maintenance of Academic Static Analyzers (preprint).

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

Milla Valnet, Raphaël Monat, Antoine Miné (2023). Analyse statique de valeurs par interprétation abstraite de programmes fonctionnels manipulant des types algébriques récursifs. JFLA.

HAL

See all publications

Recent Talks

Easing implementation and maintenance of academic static analyzers

06/06/24 Venice, Italy

Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law

11/04/24 Luxembourg

Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution)

08/04/24 Luxembourg

Lessons Learned Along the Path of an Early Career Researcher

07/04/24 Luxembourg

Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law

23/02/24 IRISA

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:

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

SOAP 2024 (chair 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

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

J’ai été jury en Juin 2023 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.
Depuis Mars 2022, je suis membre du “collège logiciel” du Comité National pour la Science Ouverte.

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, PhD student (starting Sep. 2024), co-advised by Aymeric Fromherz and Patrick Baillot.

Past students

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é.

Funded Projects

ANR-JCJC RAISIN: Resource-Aware conservatIve StatIc aNalysis

Inria-AEx AVoCAT: Automated Verification of Catala programs

Awards

ETAPS 2024 best tool paper award for “Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law”.
SV-Comp 2024 Gold Medal in the “Software Systems” category.
SV-Comp 2023 Bronze Medal in the “Software Systems” category.
ECOOP 2023 Distinguished Reviewer Award.
SOAP 2020 Best Presentation Award for “Value and Allocation Sensitivity in Static Python Analyses”.

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.
- 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.