Description
Date depot: 1 janvier 1900
Titre: Analyse Statique de Programmes Multi-threadés Dynamiques
Encadrant :
Frédéric PESCHANSKI (LIP6)
Directrice de thèse:
Michèle SORIA (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
L’{{analyse statique}} permet, avant l’exécution des programmes, de détecter des erreurs éventuelles, ou de façon complémentaire de garantir des propriétés sur leur comportement. Un exemple typique d’analyse statique concerne le typage des programmes.
Il existe de nombreuses méthodes - en général basées sur des formalismes à fort ancrage mathématique - permettant de concevoir des algorithmes puis des outils d’analyse statique de programmes.
En collaboration avec l’Université libre de Bruxelles et le laboratoire IBisc de l’Université d’Evry, nous avons développé des formalismes - la famille des {pi-graphes} - permettant de modéliser des systèmes concurrents et, surtout, dynamiques (création/destruction dynamiques de ressources - processus et canaux de communication entre processus). Ces formalismes ont été conçus pour offrir un fort potentiel d’analyse statique (équivalences comportementales, vérifications de propriétés temporelles, analyse de divergence et de deadlock, etc.)
Dans le cadre de cette thèse, nous souhaitons {{développer l'algorithmique}} sous-jacente des analyses statiques que nous avons développées - pour l'instant à un niveau théorique - dans le cadre du projet. On s'intéressera notamment au calcul efficace de bisimulation par raffinement de partition, ainsi qu'aux techniques locales et globales pour la vérification de propriétés exprimées en logiques temporelles (co-)récursives : mu-calcul, etc. Dans un second axe complémentaire de recherche, on s'intéressera à la problématique de détection automatique de terminaison/divergence de programme en exploitant la gestion fine et explicite des ressources dynamiques dans les formalismes employés.
Doctorant.e: Deharbe Aurelien