Shape Analysis for Unstructured Sharing

Huisong Li 1 Xavier Rival 1 Bor-Yuh Evan Chang 2
1 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt
Abstract : Shape analysis aims to infer precise structural properties of imperative memory states and has been applied heavily to verify safety properties on imperative code over pointer-based data structures. Recent advances in shape analysis based on separation logic has leveraged sum-marization predicates that describe unbounded heap regions like lists or trees using inductive definitions. Unfortunately, data structures with un-structured sharing, such as graphs, are challenging to describe and reason about in such frameworks. In particular, when the sharing is unstructured, it cannot be described inductively in a local manner. In this paper, we propose a global abstraction of sharing based on set-valued variables that when integrated with inductive definitions enables the specification and shape analysis of structures with unstructured sharing.
Type de document :
Communication dans un congrès
Springer. Static Analysis - 22nd International Symposium, Sep 2015, Saint-Malo, France. pp.19, 2015, 〈10.1007/978-3-662-48288-9_6〉
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01249418
Contributeur : Xavier Rival <>
Soumis le : vendredi 1 janvier 2016 - 12:58:42
Dernière modification le : jeudi 11 janvier 2018 - 06:25:39
Document(s) archivé(s) le : jeudi 7 avril 2016 - 16:59:03

Fichier

sharing-sas15.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Huisong Li, Xavier Rival, Bor-Yuh Evan Chang. Shape Analysis for Unstructured Sharing. Springer. Static Analysis - 22nd International Symposium, Sep 2015, Saint-Malo, France. pp.19, 2015, 〈10.1007/978-3-662-48288-9_6〉. 〈hal-01249418〉

Partager

Métriques

Consultations de la notice

155

Téléchargements de fichiers

69