INDIGO Home University of Illinois at Urbana-Champaign logo uic building uic pavilion uic student center

Verification of Multi-Linked Heaps

Show simple item record

Bookmark or cite this item: http://hdl.handle.net/10027/8306

Files in this item

File Description Format
PDF MultiLinkedHeaps.pdf (350KB) (no description provided) PDF
Title: Verification of Multi-Linked Heaps
Author(s): Balaban, Ittai; Pnueli, Amir; Sa’ar, Yaniv; Zuck, Lenore D.
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. 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).
Issue Date: 2012-05
Publisher: Elsevier
Citation Info: Balaban, I., Pnueli, A., Sa'ar, Y., & Zuck, L. D. 2012. Verification of multi-linked heaps. Journal of Computer and System Sciences, 78(3): 853-876. DOI: 10.1016/j.jcss.2011.08.003
Type: Article
Description: NOTICE: 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
URI: http://hdl.handle.net/10027/8306
ISSN: 0022-0000
Date Available in INDIGO: 2012-05-09
 

This item appears in the following Collection(s)

Show simple item record

Statistics

Country Code Views
United States of America 106
China 56
Japan 4
United Kingdom 3
Netherlands 3

Browse

My Account

Information

Access Key