Sciweavers

Share
VMCAI
2007
Springer

Shape Analysis of Single-Parent Heaps

10 years 7 months ago
Shape Analysis of Single-Parent Heaps
We define the class of single-parent heap systems, which rely on a singly-linked heap in order to model destructive updates on tree structures. This encoding has the advantage of relying on a relatively simple theory of linked lists to support abstraction computation. To facilitate the application of this encoding, we provide a program transformation that, given a program operating on a multi-linked heap without sharing, transforms it into one over a single-parent heap. It is then possible to apply shape analysis by predicate and ranking abstraction as in [2]. The technique has been successfully applied on examples with trees of fixed arity (balancing of and insertion into a binary sort tree).
Ittai Balaban, Amir Pnueli, Lenore D. Zuck
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where VMCAI
Authors Ittai Balaban, Amir Pnueli, Lenore D. Zuck
Comments (0)
books