Etude et définition des modèles sémantiques adéquats pour la répresentation des programmes concurrents dynamiques.

Il n'y a pas à ce jour des modèles permettant à la fois de capter de manière précise et aisée la sémantique des programmes avec du multi-threading, de la récursion et de la mémoire dynamique, et de réaliser des vérifications automatiques pertinentes. En effet, les modèles existants visent séparément chacun des aspects. Les approches qui consistent à baser l'analyse sur le produit cartesien des modèles ne permettent pas de modéliser de manière fidèle les interdépendances. Ceci conduit à des résultats d'analyse trop conservateurs et imprécis dont l'utilité pratique est très faible. Il est donc necessaire de développer des représentations symboliques et des domaines abstraits qui permettent de représenter des ensembles infinis de configuration de manière effective. Ces représentations doivent avoir un problème de satisfiabilité décidable et être doivent fermées pas les opretations booléennes.