Analyse Statique et OPTimisation – ASOPT

ASOPT est un projet de recherche fondamentale, impliquant du développement logiciel à des fins d'expérimentation et de dissémination. L'analyse statique de programmes consiste au fond à rechercher des invariants de programme : des propriétés dont on sait qu'elles sont valides pour toute exécution. Ces invariants peuvent souvent s'exprimer par des formes géométriques. Par exemple, les vecteurs de variables d'indices de boucles imbriquées appartiennent le plus souvent à des formes simples telles que des triangles ou des polyèdres convexes. La plupart des techniques d'interprétation abstraite utilisent ces propriétés géométriques afin d'obtenir des invariants de façon automatique. De nombreuses techniques d'interprétation abstraite essayent de trouver de « bons » paramètres, sinon des paramètres optimaux, pour une forme géométrique vérifiant certaines contraintes , ceci s'applique non seulement à des abstractions purement numériques (pour des variables numériques de programmes), mais aussi aux abstractions de structures de données (tableaux et formes plus compliquées). On peut souvent résoudre ce type de problèmes par des techniques d'optimisation, ce qui ouvre la possibilité d'exploiter de nombreux résultats de recherche opérationnelle. La raison d'être de ce projet est le développement de nouveaux domaines abstraits et de nouvelles méthodes de résolution afin d'améliorer la qualité des analyses de programmes, spécialement en ce qui concerne les programmes de contrôle embarqués, et, à plus long terme, les programmes de simulation numérique. Dans ce but, le projet rassemblera des experts en analyse statique, optimisation, et théorie des jeux et du contrôle autour de certains problèmes d'analyse exprimés géométriquement, afin d'inventer, développer et expérimenter de nouvelles méthodes. Nous attendons du projet qu'il contribue de deux façons à l'état de la science et de la technique : * D'une part, les concepteurs de systèmes d'analyse statique obtiendront de nouveaux outils, améliorant tant la précision que l'efficacité des analyses. De tels progrès sont notamment nécessaires afin d'appliquer les techniques d'analyse aux problèmes industriels, souvent de grande taille. * D'autre part, les théoriciens du contrôle ou de l'optimisation rencontreront de nouveaux défis: les techniques de preuve et de vérification de programmes demandent des résultats exacts, alors que pour la plupart des applications d'optimisation, des solutions approchées suffisent, par ailleurs, certains problèmes de point fixe qui apparaissent en analyse statique sont inhabituels et particulièrement durs à résoudre pour les théoriciens des jeux, car ils n'ont pas les caractéristiques usuelles des problèmes provenant du monde physique.