Establishing Local Temporal Heap Safety Properties
with Applications to Compile-Time Memory Management

We present a framework for statically reasoning about temporal heap
safety properties.
We focus on local temporal heap safety properties, in which the
verification process may be performed for a program object
independently of other program objects.
We apply our framework to produce new conservative static algorithms for
compile-time memory management, which prove for certain program points that
a memory object or a heap reference will not be needed further.
These algorithms can be used for reducing space consumption of Java
programs.
We have implemented a prototype of our framework, and used it to
verify compile-time memory management properties for several small,
but interesting example programs, including JavaCard programs.

[bib][ps][pdf]