Raphaël Monat
Raphaël Monat
Home
Publications
Ph.D
Talks
Software
Community Service
Teaching (fr)
Posts
Light
Dark
Automatic
Publications
Type
International Conference Paper
Workshop Paper (with program committee and article submission prior to the event)
National Conference Paper
Report
Date
2023
2021
2020
2019
2018
2017
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
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
×