Techniques de génération automatique d’invariants

Equipe
2XS, IRCICA
Responsable HDR
Gilles Grimaud
Encadrant
Samuel Hym
Contexte
On s’intéresse à la consommation mémoire de programmes dans des langages tels que Java. Pour prouver qu’un système critique ne va pas échouer par manque de mémoire, seule l’analyse du code source peut permettre d’obtenir une borne sur la quantité de mémoire qui sera effectivement consommée à l’exécution. Cette analyse n’est intéressante que si elle fournit un résultat suffisamment proche de la mémoire consommée dans les exécutions réelles pour être pertinent. Bien entendu, elle doit malgré tout être automatique dans la grande majorité des cas pour être utilisable sur des programmes de taille réaliste : une intervention humaine peut être indispensable pour supporter les points les plus subtiles d’un programme mais doit s’y limiter.
Problématique
Un des points essentiels pour obtenir une bonne approximation est le traitement des boucles. Pour apporter une solution à ce problème, nous utilisons les invariants de boucles : en utilisant les invariants d’un nid de boucles il est en général possible de borner son nombre d’itérations. Nous nous intéressons donc aux méthodes de génération automatique d’invariants. Plusieurs pistes sont suivies sur cette problématique : certains travaux explorent des techniques hybrides, utilisant quelques exécutions du code pour trouver des invariants possibles, puis les vérifiant ; d’autres utilisent uniquement le code source pour produire des invariants de plus en plus sophistiqués.
Travail à réaliser
On étudiera les travaux de recherche existant pour faire un panorama des techniques d’inférences d’invariant existantes, en liant, dans la mesure du possible, chaque technique au type de programme qu’elle est apte à traiter. On pourra aussi étudier comment mettre en pratique ces différentes méthodes d’inférence, en particulier comment exploiter les méthodes dynamiques pour obtenir des invariants de méthodes et non de programmes complets. Enfin, on pourra également voir comment combiner ces différentes méthodes, notamment comment choisir la ou les méthodes à utiliser suivant le programme, ou le fragment de programme, que l’on considère.
Bibliographie