Sciweavers

Share
IGPL
2006

Verifying Temporal Heap Properties Specified via Evolution Logic

10 years 6 months ago
Verifying Temporal Heap Properties Specified via Evolution Logic
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. 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 ion to be modelled naturally. The paper also presents an abstract-interpretation algorithm that automatically verifies temporal properties expressed using the logic.
Eran Yahav, Thomas W. Reps, Shmuel Sagiv, Reinhard
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where IGPL
Authors Eran Yahav, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm
Comments (0)
books