rmonat.fr Open in urlscan Pro
35.185.44.232  Public Scan

Form analysis
0 forms found in the DOM

Text Content

SEARCH




Raphaël Monat
Raphaël Monat
 * Home
 * Publications
 * Ph.D
 * Talks
 * Community Service
 * Students
 * Contact

 * 
 * Light Dark Automatic


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

 * 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, 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

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

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, M2 intern (Oct. 2023 – March 2024), co-advised by Aymeric
   Fromherz.


PAST STUDENTS

 * 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

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.
   * Notebook enveloppe convexe à remplir
   * Notebook arbres rouge-noir à remplir
   * Introduction aux notebooks jupyter
   * Raccourcis markdown
 * 2I008 : programmation fonctionnelle en OCaml
 * 3I018 : compilation.


RECENT POSTS


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

 * raphael DOT monat AT inria DOT fr
 * Bâtiment ESPRIT, avenue Paul Langevin, Villeneuve-d'Ascq, 59650


+−


Leaflet | © OpenStreetMap

Last updated 11/06/2024.

Published with Wowchemy and relying on GoHugo

CITE

×



Copy Download