Publications

CUTECat: Concolic Execution for Computational Law

Many legal computations, including the amount of tax owed by a citizen, whether they are eligible to social benefits, or the wages due …
Preprint

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