This paper addresses the problem of establishing temporal
properties of programs written in languages, such as Java, that
make extensive use of the heap to allocate---and deallocate---new
objects and threads. Establishing liveness properties is a
particularly hard challenge. One of the crucial obstacles is that
heap locations have no static names and the number of heap
locations is unbounded. The paper presents a framework for the
verification of Java-like programs. Unlike classical model
checking, which uses propositional temporal logic, we use
first-order temporal logic to specify temporal properties of heap
evolutions; this logic allows domain changes to be expressed,
which permits allocation and deallocation to be modelled
naturally. The paper also presents an abstract-interpretation
algorithm that automatically verifies temporal properties
expressed using the logic.