Analyse statique.

Les méthodes de shape analysis consistent a calculer, de façon approximative, les topologies des configurations de mémoire générées par un programme. A partir de cette information, il est possible ensuite de déduire si un objet est partagé ou s'il fait partie d'un cycle. Ceci sert a optimiser la vitesse d'exécution du programme, par exemple utilisant des algorithmes de glanage de cellules moins coûteuses pour les structures non-circulaires. D'une autre part, les techniques de escape analysis estiment le domaine de visibilité d'un objet, au cours d'une séquence d'appels récursives de fonctions. Ceci est utile pour allouer certains objets locaux directement sur la pile du thread ou par régions, facilitant ainsi la gestion de la mémoire.

Les enjeux pour que les techniques d'analyse statique soient appliquées a la vérification de programmes sont essentiellement les suivantes :

• La nécessité d'avoir un langage pour décrire des configurations de mémoire (listes, arbres, circularité, etc) afin de pouvoir exprimer des propriétés temporelles par rapport à ce genre de propositions. Un tel langage pourraient s'appuyer sur une logique. Dans ce cas, il est important de trouver les sous-ensembles décidables.
• La paramétrisation de l'abstraction par rapport à une propriété concernant la configuration dynamique de la mémoire. La paramétrisation est importante pour la génération automatique des abstractions et pour le raffinement, idéalement guidé par un scénario d'erreur.