1

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 mixing these two languages; we focus on the C analysis here. It provides a novel way to combine abstract domains, in …

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. For example, developers may want to combine high-level Python code with low-level, performance-oriented C code. In fact one …

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 …

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 …