[M1R 2012-2013] Algoritmique de graphes et analyse de programmes avec mémoire dynamique


Laboratoire : LIAFA
Equipe : Vérification
Encadrant : Mihaela Sighireanu ( http://www.liafa.univ-paris-diderot.fr/~sighirea )

Contexte scientifique : L'analyse de programmes par interprétation abstraite calcule de façon sûre des propriétés vraies pour toutes les exécutions de programmes, à l'aide de représentations symboliques (polyèdres convexes, formules de logique, automates finis...) de sur-ensembles des états possibles du programme. La difficulté consiste à garder une bonne précision (obtenir des petits invariants, permettant de démontrer les propriétés désirées) tout en gardant une bonne complexité (temps et espace).

Pour l'analyse de programmes avec mémoire dynamique, plusieurs représentations symboliques existent. Par exemple, pour les programmes manipulant des listes simplement chaînées, les graphes fonctionnels (graphes dirigés dont chaque noeud à au plus un arc sortant) sont une représentation efficace, comme le montre l'outil d'analyse Celia développé au LIAFA.

Sujet : Pour les types liste plus complexes, comme les listes doublement chaînes ou les multi-listes, des représentations basées sur des gaphes dirigés étendus ont été proposés, par exemple en [Saveluc12]. Ces représentations peuvent être également étendu aux listes imbriquées, i.e., listes de listes. Cette extension nécessite des algorithmes efficaces sur les graphes. Le sujet du stage est d'adapter les algorithmes classiques sur les graphes aux représentations utilisées pour les listes et de les intégrer dans une bibliothèque utilisée par les outils d'analyse par interprétation abstraite.

Connaissances préalables souhaitées :