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.