< Retour au sommaire
Analyse de forme avec abstraction de contenu
Josselin Giet le
Lieu: Amphi 33
Suivre en visio
Abstract
Les analyses de formes basées sur la logique de séparation
utilisent des prédicats inductifs pour synthétiser des propriétés
générales sur les structures de données inductives non bornées comme les
listes ou les arbres.
Ces prédicats sont suffisamment expressifs pour prouver l’absence
d’erreurs dues à une manipulation erronée de la mémoire, ainsi que la
préservation des invariants structurels de la structure de données.
Toutefois, ils oublient toute information concernant le contenu stocké
dans ces structures.
Dans cet exposé, nous décrivons un domaine abstrait de décrire des
séquences de valeurs de taille non bornée, et capable d’exprimer des
propriétés sur leur taille, ou leurs valeurs extrêmes.
Ensuite, nous décrivons un produit réduit entre ce domaine et un domaine
de forme basé sur la logique de séparation.
Enfin, nous montrons comment l’analyse obtenue permet
la vérification de
la correction fonctionnelle partielle de fonctions sur les listes et les
arbres.