Index

L'interprétation abstraite est une méthode d'analyse statique inventée en 1976 par Patrick Cousot. Elle est utilisée pour prouver et découvrir des propriétés sur des programmes. Les propriétés ainsi prouvées peuvent servir à démontrer la validité d'un logiciel, ou d'améliorer ses performances.

Pour chaque type de propriété que l'on cherche à prouver sur un programme, on essaie de construire un domaine abstrait dans lequel s'effectueront les calculs. Ces domaines abstraits peuvent ensuite être utilisés dans des méthodes d'interprétation abstraite.

Le choix des domaines abstraits influe sur la précision de l'analyse, et sur le temps qu'elle requiert. Pour certaines propriétés, avec le bon choix de domaine, il est possible d'analyser efficacement les programmes. Il devient alors réaliste d'analyser des logiciels entiers. En général, il est nécessaire de trouver des critères pertinents pour déterminer quelles propriétés doivent être conservées, et quelles propriétés doivent être abstraites.

L'utilisation de tableaux ou de structures de données complexes dans les programmes rend l'analyse notablement plus difficile. Il est impossible de considérer chaque élément de tableau, ou chaque structure allouée dynamiquement puisque leur nombre est inconnu statiquement. Il faut alors trouver une manière pertinente de considérer des sous ensembles d'éléments de tableau ou de structures. C'est ce qui constitue le principal de mes objectifs de recherche actuels.

Analyse de propriétés non positionnelles sur les tableaux.

Stage de Master / DEA, MPRI, Verimag, encadré par Nicolas Halbwachs
Rapport - Slides

En 2008, Nicolas Halbwachs et Mathias Péron ont proposé une méthode efficace capable de découvrir sans aide de l'utilisateur des propriétés générales sur les tableaux. En particulier capable de découvrir que le résultat d'un tri par insertion est un tableau trié. Pour compléter ce résultat, il est nécessaire de prouver que l'algorithme retourne non seulement un tableau trié, mais également que ce tableau contient, réordonnées, les mêmes valeurs que le tableau initial. Autrement dit, le tableau résultat doit être une permutation du tableau donné en entrée.

On cherche alors à découvrir des propriétés sur le multiensemble des valeurs d'un tableau. On veut savoir si ce multiensemble a été conservé ou modifié.

Le résultat d'une telle analyse peut être surprenant, comme dans l'exemple suivant. Il s'agit d'un échange de trois éléments d'un tableau aux indices i, j et k en deux étapes. Pour qu'il soit correct, il faudrait s'assurer que le multiensemble des valeurs du tableau est conservé par l'algorithme. Or ce n'est pas toujours le cas, en particulier lorsque i = k.