%0 Conference Proceedings
%T Unbounded Allocation in Bounded Heaps
%+ Leiden Institute of Advanced Computer Science [Leiden] (LIACS)
%+ Centrum voor Wiskunde en Informatica (CWI)
%A Rot, Jurriaan
%A Boer, Frank, De
%A Bonsangue, Marcello
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 5th International Conference on Fundamentals of Software Engineering (FSEN)
%C Tehran, Iran
%Y Farhad Arbab
%Y Marjan Sirjani
%I Springer Berlin Heidelberg
%3 Fundamentals of Software Engineering
%V LNCS-8161
%P 1-16
%8 2013-04-24
%D 2013
%R 10.1007/978-3-642-40213-5_1
%Z Computer Science [cs]Conference papers
%X 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.
%G English
%2 https://inria.hal.science/hal-01514664/document
%2 https://inria.hal.science/hal-01514664/file/978-3-642-40213-5_1_Chapter.pdf
%L hal-01514664
%U https://inria.hal.science/hal-01514664
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC2
%~ IFIP-WG2-2
%~ IFIP-FSEN
%~ IFIP-LNCS-8161