# 1

## 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 the French Public Finances Directorate (DGFiP). This algorithm relies on a legacy custom language and compiler …

## 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 powerful and permissive high-level syntax. Our work aims at detecting statically and automatically type errors. As …

## 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 analyzer soundly overapproximates the behavior of C programs that do not contain any dynamic code loading, longjmp …

## É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 d'un foyer fiscal. Afin de recouvrer l'impôt, cette fonction est implémentée sous la forme d'un algorithme par la Direction …

## 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 to achieve a high degree of modularity and extensibility by considering value abstractions for numeric, pointer, …

## 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 and scientific computing. Due to the discrepancy between continuous reals and discrete finite-precision values, …

## 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 (assuming a sequentially consistent memory), parameterized by a choice of abstract domains and, in order to scale up, it …