Notre approche pour le développement des algorithmes d´analyse et de vérification pour les nouvelles classes de programmes s´appuie sur deux techniques existantes : l´analyse de la mémoire (shape analysis [#!shape!#] et escape analysis [#!escape!#]) et la vérification symbolique (regular model checking [#!regular!#]). Le ``shape analysis'' est une analyse statique permettant à tout point de contrôle dans le programme d´obtenir une représentation abstraite de la structure de mémoire dynamique obtenu pendant l´exécution réelle du programme. Le ``escape analysis'' permet d'approximer statiquement la portée des références aux objets. Le ``regular model checking'' est une technique de vérification permettant de calculer, de façon précise, l´ensemble d´états atteignables à partir d´un état donné. Ceci s´applique notamment aux systèmes avec du contrôle dynamique.
En partant de ces techniques, chacune qui s´applique à une classe d´aspects seulement (soit aux données, soit au contrôle dynamique), notre objectif est d´étudier, sur un plan théorique, les relations qui existent entre elles afin d´élaborer, par la suite, des nouvelles techniques composites pour traiter des problèmes plus complexes (par exemple, des données dynamiques avec multithreading).
D´un point de vue théorique les téchniques d´analyse statique ainsi que celles de model checking sont basées sur un calcul de point fixe d´une relation de transition entre des ensembles d´états. L'idée centrale de notre approche est d'exploiter au mieux leur complémentarité par rapport aux deux critères suivants :
La réalisation du projet devra surmonter un certain nombre de défis que nous détaillons ci-dessus pour chacune des techniques d'analyse :