Skip to Main content Skip to Navigation
Conference papers

Unbounded Allocation in Bounded Heaps

Abstract : In this paper we introduce a new symbolic semantics for a class of recursive programs which feature dynamic creation and unbounded allocation of objects. We use a symbolic representation of the program state in terms of equations to model the semantics of a program as a pushdown system with a finite set of control states and a finite stack alphabet. Our main technical result is a rigorous proof of the equivalence between the concrete and the symbolic semantics.Adding pointer fields gives rise to a Turing complete language. However, assuming the number of reachable objects in the visible heap is bounded in all the computations of a program with pointers, we show how to construct a program without pointers that simulates it. Consequently, in the context of bounded visible heaps, programs with pointers are no more expressive than programs without them.
Document type :
Conference papers
Complete list of metadata

Cited literature [11 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Wednesday, April 26, 2017 - 3:22:06 PM
Last modification on : Wednesday, December 20, 2017 - 5:42:07 PM
Long-term archiving on: : Thursday, July 27, 2017 - 12:59:52 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Jurriaan Rot, Frank De Boer, Marcello Bonsangue. Unbounded Allocation in Bounded Heaps. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. pp.1-16, ⟨10.1007/978-3-642-40213-5_1⟩. ⟨hal-01514664⟩



Record views


Files downloads