Shape Analysis for Unstructured Sharing

5 years 2 months ago
Shape Analysis for Unstructured Sharing
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 summarization predicates that describe unbounded heap regions like lists or trees using inductive definitions. Unfortunately, data structures with unstructured 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 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.
Huisong Li, Xavier Rival, Bor-Yuh Evan Chang
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where SAS
Authors Huisong Li, Xavier Rival, Bor-Yuh Evan Chang
Comments (0)