Interacting via the Heap in the Presence of Recursion

Almost all modern imperative programming languages include operations

for dynamically manipulating the heap, for example by allocating and

deallocating objects, and by updating reference fields. In the presence

of recursive procedures and local variables the interactions of a

program with the heap can become rather complex, as an unbounded number

of objects can be allocated either on the call stack using local variables,

or, anonymously, on the heap using reference fields. As such a static

analysis is, in general, undecidable.



In this paper we study the verification of recursive programs with unbounded

allocation of objects, in a simple imperative language for heap manipulation.

We present an improved semantics for this language, using

an abstraction that is precise. For any program with a bounded

visible heap, meaning that the number of objects reachable from

variables at any point of execution is bounded, this abstraction

is a finitary representation of its behaviour, even though

an unbounded number of objects can appear in the state.

As a consequence, for such programs model checking is decidable. Finally we

introduce a specification language for temporal properties

of the heap, and discuss model checking these properties

against heap-manipulating programs.