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
or 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. 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
Javalike 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:
PDF.)