ASOPT

ASOPT (Static Analysis and OPTimisation) is a fundamental research project, whose aim is to develop new resolution techniques to improve the quality of static program analysis, especially for embedded control programs which high-level of criticality, and, in the longer run, for numerical simulation programs. It exploits the
abstract interpretation method, which allows one to determine a priori
some invariants of a program (properties which are valid for all
executions). These invariants can often be expressed geometrically.
For instance, the index variables in nested loops typically lie within
convex polyhedra. Then, methods from convex programming and game
theory can be applied to find invariants. The project develops and
exploits the emerging interactions between global optimization, game
theory, and static analysis, in order to compute accurate invariants.