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 metadatas

Cited literature [11 references]  Display  Hide  Download

https://hal.inria.fr/hal-01514664
Contributor : Hal Ifip <>
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

File

978-3-642-40213-5_1_Chapter.pd...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Jurriaan Rot, Frank 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⟩

Share

Metrics

Record views

139

Files downloads

164