Title: Shape Analysis of Single-Parent Heaps


(NYU-CS-TR885)

Authors: Ittai Balaban, Amir Pnueli, Lenore D. Zuck

Abstract:
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 in order 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
[BPZ05]. The technique has been successfully applied on
examples with trees of fixed arity (balancing of and insertion into
a binary sort tree).