Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download
Contributor : Xavier Rival <>
Submitted on : Friday, January 1, 2016 - 12:58:42 PM
Last modification on : Tuesday, May 4, 2021 - 2:06:02 PM
Long-term archiving on: : Thursday, April 7, 2016 - 4:59:03 PM


Files produced by the author(s)




Huisong Li, Xavier Rival, Bor-Yuh Evan Chang. Shape Analysis for Unstructured Sharing. SAS 2015 - 22nd International Symposium on Static Analysis, Sep 2015, Saint-Malo, France. pp.90-108, ⟨10.1007/978-3-662-48288-9_6⟩. ⟨hal-01249418⟩



Record views


Files downloads