News: Next meeting: Nancy, journées ParisTIC, 22-24 November 2006 (See our PDF poster)
- Program analysis
- Abstract interpretation
- Numerical properties
- Runtime errors
- Linear relation analysis
Five research teams, all active in abstract interpretation, are joining forces to eliminate the stumbling blocks limiting the effectiveness of current static analyses used:
- to check statically safety and security properties,
- and to identify and locate origins of failures.
To overcome calculability limit, approximate analyses must be used. But the current resulting accuracy must be improved to reduce areas of uncertainty, which may reach more than 98 % of an application analyzed by commercially available automatic tools. Execution and space, as well as accuracy, must be controlled together: an analysis lasting a whole night and requiring more than 4GB of main memory does not have the same industrial impact as a five minute long analysis runing on a laptop.
Stumbling blocks 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 domain, 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? Breakthoughs 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 defined 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.
Results (Draft stage)
The main result of the project is a common APRON API for numerical abstract domain. Three libraries implement this API, one for intervals, one for polyhedra and the other one for octagons. Two bindings are available: C and OCaml. The libraries and the documentation are available for download by clicking the corresponding link on the left.
A polyhedral benchmarking environment was developped by Duong Nguyen and made available online (Polybench). This environment was used to compare different algorithms and different implementations of polyhedral operators such as satisfiability and convex hull.
VERIMAG provided a simple test case that turned out to be very useful to understand the differences (in French) between the iterative widening approach used by some partner to handle loops and the direct algorithm used by PIPS, the modular static analyzer developped at Ecole des mines.