Description
Date depot: 1 janvier 1900
Titre: Analyse statique de programmes parallèles avec variables numériques
Directeur de thèse:
Emmanuel CHAILLOUX (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
La vérification formelle des systèmes concurrents est un domaine de recherche qui passionne les chercheurs depuis plus de 30 ans, mais qui, en raison de la complexité des questions abordées, reste un champ de recherche ouvert. Ces dernières années, l'évolution du matériel et des logiciels embarqués accroissent le besoin industriel de pouvoir disposer à moyen terme de programmes parallèles certifiés ``sans bug''.
De nombreuses approches de type {model checking} [4, 3, 9] ont déjà été proposées pour vérifier formellement les systèmes concurrents. Cependant, des difficultés à la fois théoriques et pratiques (explosion du nombre d'états) les obligent à ne considérer que des modèles de processus simples (processus identiques [3], mémoire finie [10], ...) et à restreindre les communications entre processus [12]. De nombreux résultats théoriques récents [2,6] témoignent de l'intérêt actuel de la communauté scientifique pour ce domaine de recherche mais ne permettent pas de définir directement un analyseur statique efficace.
L'interprétation abstraite [5] fournit un cadre théorique robuste pour définir de tels analyseurs. Ces analyseurs sont principalement conçus pour les programmes séquentiels, avec des extensions pour traiter les programmes parallèles (AstréeA [1] pour Astrée, Mthread [11] pour Frama-C,...). Nous nous proposons de poursuivre ces travaux [7,8] en considérant notamment un modèle de parallélisme plus riche (création dynamique de processus, communications FIFO, ...).
Doctorant.e: Botbol Vincent