Raphaël Monat
Raphaël Monat
Home
Publications
Ph.D
Talks
Community Service
Students
Contact
Light
Dark
Automatic
Publications
Type
International Conference Paper
Workshop Paper (with program committee and article submission prior to the event)
National Conference Paper
Journal article
Report
Date
2024
2023
2021
2020
2019
2018
2017
Easing Maintenance of Academic Static Analyzers
Academic research in static analysis produces software implementations. These implementations are time-consuming to develop and some …
PDF
arXiv
HAL
Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution)
We present advances we brought to Mopsa for SV-Comp 2024. We significantly improved the precision of our verifier in the presence of …
PDF
SV-Comp results
Slides
Editor
HAL
Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law
SCP award for the ETAPS best tool paper.
Legal expert systems routinely rely on date computations to determine the eligibility of a citizen to social benefits or whether an …
PDF
Artefact (reviewed A,F,R)
Slides
HAL
Editor
Award
Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution)
Mopsa is a multilanguage static analysis platform relying on abstract interpretation. It is able to analyze C, Python, and programs …
PDF
DOI
Validated Artefact
HAL
Slides
SV-Comp results
Analyse statique de valeurs par interprétation abstraite de programmes fonctionnels manipulant des types algébriques récursifs
Afin de prévenir les erreurs de programmation, des analyseurs statiques ont été développés pour de nombreux langages ; cependant, aucun …
HAL
Static Type and Value Analysis by Abstract Interpretation of Python Programs with Native C Libraries
In this thesis, we aim at designing both theoretically and experimentally methods for the automatic detection of potential bugs in software – or the proof of the absence thereof. This detection is done statically by analyzing programs' source code without running them.
Thesis
Slides
YouTube
Artefact
A Multilanguage Static Analysis of Python Programs with Native C Extensions
Modern programs are increasingly multilanguage, to benefit from each programming language’s advantages and to reuse libraries. …
PDF
DOI
Approved Artefact
Preprint (HAL)
Slides
Talk
Talk (YouTube)
Event
Mlang: an Open-Source Toolchain for the Income Tax Computation
Once per year, the French Directorate for Public Finances (DGFiP) computes for each citizen the amount of income tax owed to the State, …
PDF
Slides
Code (github)
JFLA proceedings
Démonstration de la plateforme Mopsa d’analyse statique de programmes par interprétation abstraite
Mopsa est un logiciel de vérification de programmes par analyse statique sûre basée sur la théorie de l’interprétation abstraite. …
PDF
JFLA proceedings
A Modern Compiler for the French Tax Code
In France, income tax is computed from taxpayers' individual returns, using an algorithm that is authored, designed and maintained by …
PDF
Slides
Video
DOI
Approved Artefact
Code (github)
HAL
Event
Value and Allocation Sensitivity in Static Python Analyses
Best presentation award.
Sound static analyses for large subsets of static programming languages such as C are now widespread. For example the Astrée static …
PDF
DOI
Slides
Talk (video)
Demo (video)
Talk (YouTube)
Event
Static Type Analysis by Abstract Interpretation of Python Programs
Python is an increasingly popular dynamic programming language, particularly used in the scientific community and well-known for its …
PDF
DOI
Approved Artefact
Slides
Talk (video)
Talk (YouTube)
Mopsa Project
Mopsa's Gitlab
Event
Étude formelle de l’implémentation du code des impôts
Le code des impôts définit dans son texte législatif une fonction mathématique permettant de calculer l’impôt sur le revenu …
Preprint
PDF
Code
Slides
Proceedings
Combinations of reusable abstract domains for a multilingual static analyzer
We discuss the design of Mopsa, an ongoing effort to design a novel semantic static analyzer by abstract interpretation. Mopsa strives …
PDF
DOI
BIB
Slides by Antoine Miné
Event
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
Being able to soundly estimate roundoff errors of finite-precision computations is important for many applications in embedded systems …
Preprint
PDF
Code
BIB
DOI
Event
Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions
We present a static analysis by abstract interpretation of numeric properties in multi-threaded programs. The analysis is sound …
Preprint
PDF
Code
Slides
BIB
DOI
Event
Cite
×