Automatic Verification of Temporal Properties of Concurrent Heap-Manipulating Programs using Evolution
Logic

Yahav, E., Reps, T., Sagiv, M. and Wilhelm R

TR 338/02, School of Computer Science, Tel Aviv University, July 2002

Abstract

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. We use first-order modal logic to specify
temporal properties of heap evolutions;
this logic is a simple variant of existing first-order
modal logics that allow expressing universe changes. The paper also
presents an abstract-interpretation algorithm that automatically
verifies temporal properties expressed using the logic.