recherche

05/12/2010

Thèse

Ma thèse porte sur la vérification statique de programmes numériques. Employé par le CNRS, j'effectue mes travaux dans l'équipe synchrone du laboratoire Vérimag sous la direction de Nicolas Halbwachs.

Nous avons proposés [PLDI'08] une analyse statique par interprétation abstraite permettant de découvrir des propriétés sur le contenu des tableaux. L'analyse est paramétrée par deux domaines abstraits : un domaine numérique pour manier des propriétés sur les variables scalaires qui indexent les tableaux; un autre domaine abstrait pour manier des propriétés sur le contenu des tableaux, qui n'ai pas nécessairement numérique. Des propriétés relationelles sur les cellules des tableaux peuvent être exprimées : ∀ k ∈ [2,n], A[k] ≥ A[k-1].
Bien que la classe de programmes pour laquelle l'analyse donne de bons résultats est restreinte (les boucles portant sur une variable indiçant un tableau ne peuvent progresser que d'unité en unité) des algorithmes intéressant tombe dans cette classe : le tri par insertion, la phase de segmentation de QuickSort, des algorithmes basés sur une sentinelle, etc.

Nous avons introduit [VMCAI'07] un domaine numérique abstrait permettant d'exprimer la non-égalité de variables. Ces invariants (x ≠ y, x ≠ 0) sont couplés au domaine des zones afin de pouvoir déduire des invariants non-triviaux (x > z &ge y ⇒ x ≠ y). L'algorithmique et la représentation du domaine est basée sur celles des DBMs, d'où son nom, disequalites Difference-Bound Matrices (dDBM).