Comparaison de définitions inductives en logique de séparation et analyse statique (Antique, Xavier Rival) — sujet déjà choisi

La logique de séparation permet de décrire des propriétés sur les structures de données utilisées par les programmes. On peut par exemple décrire des listes ou des arbres avec ou sans partage à l'aide de formule logiques. Dans le cas général, on doit utiliser des formules récursives. En paramétrant ces définitions, on peut décrire des structures complexes (listes triées, arbres équilibrés, etc). Ces formules peuvent ensuite être utilisées pour vérifier de manière automatique, par analyse statique, que des programmes sont corrects, c'est-à-dire qu'ils ne risquent pas de planter suite à une erreur à l'exécution ou de briser des invariants structurels. L'analyse calcule des invariants sous la forme de formules logiques particulières, puis utilise celles-ci afin de vérifier des propriétés sémantiques des programmes.

Une difficulté majeure est que l'analyse peut être amenée à affaiblir des formules de manière automatique, par un raisonnement global. Par exemple, si une structure est une liste doublement chaînée, c'est aussi une liste simple.

Les techniques d'analyse actuelles savent bien effectuer un tel affaiblissement de manière locale, mais pas de manière globale, c'est-à-dire sur l'ensemble d'une structure inductive. Le but de ce sujet est précisément de remédier à cela. Plus précisément, on s'intéressera aux tâches suivantes :

  • étude d'exemples ;
  • formalisation et implémentation d'un algorithme de preuve automatique d'implication à base d'interprétation abstraite ;
  • recherche d'algorithmes d'instantiation des paramètres des définitions inductives ;
  • recherche d'heuristiques permettant de mettre en oeuvre des affaiblissements au cours d'une analyse.

Contact : Xavier Rival

Last modified: Thursday, 27 September 2018, 12:05 AM