Verifying Temporal Heap Properties Specified via Evolution Logic

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.