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).

• Type: Conference
• Year: 2007
• Where: VMCAI
• Authors: Ittai Balaban, Amir Pnueli, Lenore D. Zuck
• Keywords: Single-parent Heap, Single-parent Heap Systems, Singly-linked Heap, Software Engineering, VMCAI 2007