Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-38856-9_10 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Data structure,Separation logic,Linked list,Computer science,Graph homomorphism,Theoretical computer science,Homomorphism,Operator (computer programming),Tree automaton,Shape analysis (digital geometry) | Conference | 7935 |
ISSN | Citations | PageRank |
0302-9743 | 5 | 0.43 |
References | Authors | |
19 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Cezara Dragoi | 1 | 62 | 7.10 |
| Constantin Enea | 2 | 249 | 26.95 |
| Mihaela Sighireanu | 3 | 658 | 37.99 |