Article ID Journal Published Year Pages File Type
430732 Journal of Computer and System Sciences 2012 24 Pages PDF
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).

► Definition of SPH – multi-linked heap systems with destructive updates and no-sharing. ► Predicate and ranking abstraction to SPH to prove safety and liveness property. ► Small model theorem for abstraction of SPH. ► Examples for analysis of SPH using abstractions.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
, , , ,