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.