Objectives
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 modeled? How can we automatically control the trade-off between accuracy and speed by switching the 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? Breakthroughs at the conceptual level will require that technological barriers be pushed too: how to design a generic analyzer performing interdependent analyzes? How can new abstract domains defined and implemented by one team be readily used by another? The validation of the conceptual breakthrough will also require experimental breakthroughs: can we defined abstract interpretation case benchmarks and abstract domain benchmarks?
Partners
- CRI/ENSMP
- ENS
- IRISA/VERTECS
- Polytechnique
Verimag people involved
- Nicolas Halbwachs
