Stage de DEA:
Adaptation des difference bound matrices à l'analyse de programmes

[English version]

Présentation

Ce stage a été effectué dans le cadre du DEA Sémantique, preuves et langages au sein du LIENS, le laboratoire d'informatique de l' ENS de Paris, sous la direction de Patrick Cousot.

Mots-clefs: analyse de programmes, interprétation abstraite, difference bound matrices (DBM), invariants numériques.

Résumé

Nous présentons, dans ce rapport, une nouvelle méthode d'analyse statique de programmes. Cette analyse calcule de manière automatique des invariants sur les variables numériques d'un programme, à l'instar des méthodes classiques d'analyse d'intervalles ou d'inégalités linéaires. Plus précisément, les invariants que nous trouvons sont de la forme ±x ±y ≤ c (que nous appellerons contrainte de somme ou de différence de deux variables), où x et y sont des valeurs de variables et c est une constante numérique.

Nous utilisons des difference bound matrices pour représenter les ensembles de contraintes de somme ou de différence de deux variables. Leur complexité en espace est, au pire, en O(n²), n étant le nombre de variables dans le programme, et les algorithmes qui les manipulent ont une complexité, au pire, en O(n³). La sûreté de cette analyse est prouvée dans le cadre formel de l'interprétation abstraite en utilisant des correspondances de Galois entre treillis complets.

Bien que les difference bound matrices soient très utilisées pour le model-checking d'automates temporisés, il nous a fallu introduire de nombreux opérateurs (élargissement, affectation, garde,...) pour les rendre utilisables dans le cadre de l'interprétation abstraite. De plus, comme les difference bound matrices n'ont été utilisées, jusqu'à présent, que pour représenter les contraintes de la forme x-y ≤ c, nous avons dû les étendre pour pouvoir représenter les contraintes de sommes aussi bien que les contraintes de différence de deux variables.

Domaine d'un ensemble de contraintes de somme ou de différence de deux variables.

Rapport de DEA

• Vous pouvez télécharger mon rapport de DEA au format Postscript compressé (285 Ko) ou au format Acrobat PDF (579 Ko), anglais uniquement.
• Également disponibles, les transparents de ma soutenance de DEA au format Postscript compressé (116 Ko) ou au format Acrobat PDF (170 Ko), en français.

Implémentation

Ce travail théorique à donné le jour à une une bibliothèque (page en anglais), disponible gratuitement.

Bibliographie