---
res:
bibo_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.\r\n@eng"
bibo_authorlist:
- foaf_Person:
foaf_givenName: Cezara
foaf_name: Dragoi, Cezara
foaf_surname: Dragoi
foaf_workInfoHomepage: http://www.librecat.org/personId=2B2B5ED0-F248-11E8-B48F-1D18A9856A87
- foaf_Person:
foaf_givenName: Constantin
foaf_name: Enea, Constantin
foaf_surname: Enea
- foaf_Person:
foaf_givenName: Mihaela
foaf_name: Sighireanu, Mihaela
foaf_surname: Sighireanu
bibo_doi: 10.1007/978-3-642-38856-9_10
bibo_volume: 7935
dct_date: 2013^xs_gYear
dct_language: eng
dct_publisher: Springer@
dct_title: Local shape analysis for overlaid data structures@
...