Abstract FR:

Le cadre de cette thèse est l'analyse statique modulaire par interprétation abstraite de logiciels en vue de leur vérification automatique. Nous nous intéressons en particulier aux programmes comportant des objets alloués dynamiquement sur un tas et repérés par des pointeurs. Le but final étant de trouver des erreurs dans un programme (problèmes de déréférencements et d'alias) ou de prouver qu'un programme est correct (relativement à ces problèmes) de façon automatique. Isthiaq, Pym, O'Hearn et Reynolds ont développé récemment des logiques de fragmentation (separation logics) qui sont des logiques de Hoare avec un langage d'assertions/de prédicats permettant de démontrer qu'un programme manipulant des pointeurs sur un tas est correct. La sémantique des triplets de la logique ({P}C{P′}) est définie par des transformateurs de prédicats de style plus faible pré-condition. Nous avons exprimé et prouvé la correction de ces plus faibles pré-conditions (wlp) et plus fortes post-conditions (sp), en particulier dans le cas de la commande while. L'avantage par rapport à ce qui est fait dans la communauté est que les wlp et sp sont définis pour toute formule alors que certaines des règles existantes avaient des restrictions syntaxiques. Nous avons rajouté des points fixes à la logique ainsi qu'une substitution retardée permettant d'exprimer des formules récursives. Nous avons exprimé les wlp et sp dans cette logique avec points fixes et prouvé leur correction. La substitution retardée a une utilité directe pour l'expression de formules récursives. Par exemple, nclist(x) = μXv. (x = nil) ∨ ∃x1, x2. (isval(x1) ∧ (x 7→ x1, x2 ∗ Xv[x2/x])) décrit l'ensemble des mémoires où x pointe vers une liste d'entiers. Le but ensuite était d'utiliser cette logique de fragmentation avec points fixes comme langage d'interface pour des analyses de pointeurs. Il s'agit de formuler une traduction des domaines de ces analyses en formules de la logique (et inversement) et d'en prouver la correction. On peut également parfois utiliser ces traductions pour prouver la correction de ces analyses. Nous avions déjà illustré cette approche pour une analyse très simple de partitionnement des pointeurs. Nous avons traduit les formules de la logique dans un nouveau langage abstrait permettant de décrire le type des valeurs associées aux variables dans la mémoire (nil, entier, bool, pointeur vers une paire de tel type, etc. ) ainsi que les relations d'aliasing et non-aliasing entre variables et entre points de la mémoire. Le principal apport est la définition de ce langage et de sa sa sémantique dans le domaine concret qui est celui utilisé pour la sémantique des formules. En particulier, les variables auxiliaires dont la sémantique est habituellement une question d'implémentation font ici explicitement part du langage et de sa sémantique. Ce langage est un produit cartésien de plusieurs sous domaines et peut être paramétré par les domaines numériques existants. Nous avons créé un sous-domaine qui est un tableau permettant de compenser le manque de précision dû à l'utilisation de graphes d'ensembles au lieu d'ensembles de graphes. Nous avons exprimé et prouvé les traductions des formules dans ce langage abstrait.