Séminaire LSL - Josselin Giet - Analyse de forme avec abstraction de contenu

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.