1. Introduction

Five research teams from Ecole des Mines de Paris, Ecole Normale Supérieure de Paris, Ecole Polytechnique, Verimag, IRISA, all active in abstract interpretation research, are dealing with problems limiting the effectiveness of current static analyses used to statically check safety and security properties, and to identify and locate origins of failures [APRb].

Many abstract domains for the analyses of numerical variables of programs, which offer common as well as specific functionalities, have been designed and used. However, approximate analyses must be used to overcome calculability limits, and using these abstract domains' engines is not problem-free. The current resulting accuracy must be improved to reduce areas of uncertainty, which may reach more than $98$ percent of an application analyzed by commercially available automatic tools [APRb]. Execution time and memory space, as well as accuracy of analyses, must be controlled together: an analysis lasting a whole night and requiring more than $4$GB of main memory does not have the same industrial impact as a five minute long analysis running on a laptop.

Existing APIs of those engines are not compatible. They are not context-of-use independent and some fundamental functionalities are not available in some implementations. It is difficult to compare those interfaces since a generic interface that would define the exact semantics of its signature is not available. For example, we can distinguish between the projection operator and the projection_and_minimize operator, or not, in the polyhedral abstract domain. Moreover, since the precision of different abstract domains and the efficiency of different implementations of the same abstract domain are not easy to compare, we need to study these questions.

Problems identified by the teams and addressed by the APRON project are at the conceptual, technological and experimental levels. How can floating point operations with rounding or non-linear expressions be mathematically modelized? How can we automatically control the trade-off between accuracy and speed by switching abstract domains by tuning the number of control points, by adding auxiliary variables to memorize part of the execution trace, by increasing the number of contexts for procedure analysis?

Breakthroughs at the conceptual level will require that technological barriers be pushed too: how to design a generic analyzer performing interdependent analyses? How can new abstract domains defined and implemented by one team be readily used by another one? The validation of the conceptual breakthrough will also require experimental breakthroughs: can we define abstract interpretation case benchmarks and abstract domain benchmarks?

The main targets for APRON analyzers are control applications with large numerical components, using floating point numbers, counters and arrays, that are intractable by finite state-based methods. These applications will be real-life applications, in the $100$ to $500$ KLOC range, with thousands of modules. Adaptative abstract interpreters are required to deliver the accuracy and the effectiveness these applications demand.

A generic analyzer performing interdependent analyses, using any available abstract domain, with experimental results is the final target. However, the APRON project is in its very first phase. The generic analyzer is divided into several layers, which are only defined at the lowest level, $0$.