Direction de recherche : Antoine MINÉ

Analyse statique modulaire précise par interprétation abstraite pour la preuve automatique de correction de programmes et pour l’inférence de contrats

Assurer le passage à l’échelle des analyseurs statiques définis par interprétation abstraite pose des difficultés. Une méthode classique d’accélération consiste en la découverte et la réutilisation de contrats satisfaits par certaines commandes du code source. Cette thèse s’intéresse à un sous-ensemble de C qui ne permet pas la récursivité, pour lequel on définit un analyseur modulaire capable d’inférer, de prouver et d'exploiter de tels contrats.
Notre analyse est défini au-dessus d’un analyseur C existant et est donc capable de manipuler des types unions, des types structures, des tableaux, des allocations de mémoire (statique et dynamique), des pointeurs, y compris l'arithmétique de pointeur et le transtypage, appels de fonction, des chaînes de caractères .... La représentation des chaînes de caractère est gérée par un nouveau domaine abstrait défini dans cette thèse.
Nous proposons de plus une technique paramétrique de transformation de la sémantique classique des domaines abstraits vers une sémantique d’ensembles hétérogènes. Cette technique ne maintient qu’un seul état abstrait numérique, par opposition au partitionnement.
Finalement, nous proposons un domaine abstrait capable de représenter des ensembles d’arbres dont les feuilles peuvent contenir des labels numériques. Cette abstraction est basée sur les langages réguliers (d'arbre), et délègue une partie de son abstraction à un domaine numérique sous-jacent.
Cette thèse s’étant déroulée au sein du projet Mopsa, nous donnons donc un aperçu de certains résultats obtenus par l’équipe pendant la thèse.

Publications 2016-2020