Introduction
ASOPT is a fundamental research project, involving software development for experimental and dissemination purposes.
Static program analysis basically consists in finding program invariants: properties that are known to hold for all executions. These invariants can often be expressed as geometric shapes. For instance, the index variables in nested loops often lie within simple shapes, such as triangles or convex polyhedra. Most abstract interpretation techniques leverage such geometrical properties in order to automatically obtain invariants.
Many abstract interpretation techniques attempt to find "good", if not optimal, parameters for a geometric shape verifying certain constraints; this not only applies to purely numerical abstractions (for numerical program variables), but also to abstractions of data structures (arrays and more complex shapes). This problem can often be addressed by optimization techniques, opening the possibility of exploiting a wide range of advanced techniques from mathematical programming.
Objectives
The purpose of this project is to develop new abstract domains and new resolution techniques to improve the quality of program analysis, especially for embedded control programs, and in the longer run, for numerical simulations programs.
Partners
Verimag People Involved
- Nicolas Halbwachs
- David Monniaux
- Valentin Perrelle
- Julien Le Guen
