MultiLinkedHeaps.pdf (342.12 kB)
Verification of Multi-Linked Heaps
journal contributionposted on 2012-05-09, 00:00 authored by Ittai Balaban, Amir Pnueli, Yaniv Sa’ar, Lenore D. Zuck
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. 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).
Publisher StatementNOTICE: this is the author’s version of a work that was accepted for publication in Journal of Computer and System Sciences. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Journal of Computer and System Sciences, [Vol 78, Issue 3, (MAY 2012)] DOI: 10.1016/j.jcss.2011.08.003