Verifying Temporal Heap Properties Specified via Evolution Logic
Eran Yahav, Thomas Reps, Mooly Sagiv, and Reinhard Wilhelm
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.
(Click here to access the paper:
PostScript,
PDF.)
University of Wisconsin