MultiLinkedHeaps.pdf (342.12 kB)
Download fileVerification of Multi-Linked Heaps
journal contribution
posted on 2012-05-09, 00:00 authored by Ittai Balaban, Amir Pnueli, Yaniv Sa’ar, Lenore D. ZuckWe 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. The technique has been successfully applied on examples with lists (reversal and bubble sort) and trees with of fixed arity (balancing of, and insertion into, a binary sort tree).