Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

Shape Analysis for Unstructured Sharing

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 Connect in order to contact the contributor
Submitted on : Friday, January 1, 2016 - 12:58:42 PM
Last modification on : Thursday, March 17, 2022 - 10:08:44 AM
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