Local Shape Analysis for Overlaid Data Structures

Dragoi, Cezara and Enea, Constantin and Sighireanu, Mihaela (2013) Local Shape Analysis for Overlaid Data Structures. Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013., 7935. pp. 150-171. ISSN 978-3-642-38855-2

[img] Text
sas13.pdf - Accepted Version
Available under License All rights reserved.
Download (291Kb)
Official URL: http://link.springer.com/chapter/10.1007/978-3-642...


We present a shape analysis for programs that manipulate overlaid data structures which share sets of objects. The abstract domain contains Separation Logic formulas that (1) combine a per-object separating conjunction with a per-field separating conjunction and (2) constrain a set of variables interpreted as sets of objects. The definition of the abstract domain operators is based on a notion of homomorphism between formulas, viewed as graphs, used recently to define optimal decision procedures for fragments of the Separation Logic. Based on a Frame Rule that supports the two versions of the separating conjunction, the analysis is able to reason in a modular manner about non-overlaid data structures and then, compose information only at a few program points, e.g., procedure returns. We have implemented this analysis in a prototype tool and applied it on several interesting case studies that manipulate overlaid and nested linked lists.

Item Type: Article
DOI: 10.1007/978-3-642-38856-9_10
Subjects: 000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems
000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems > 004 Data processing & computer science
Research Group: Henzinger Group
Depositing User: Cezara Dragoi
Date Deposited: 28 Apr 2014 09:08
Last Modified: 16 Mar 2016 11:49
URI: https://repository.ist.ac.at/id/eprint/196

Actions (login required)

View Item View Item