Heap-space inference for Java objects.

Martin Hofmann, joint work with Steffen Jost.

We consider a version of Java with imperative update and explicit deallocation in the style of C / C++. We assume a free-list from which cells are taken upon object creation and to which deallocated objects are returned for future use. Our goal is to automatically infer an upper bound as a function of the input on the size of a free-list required to successfully evaluate a program phrase.

Our analysis uses ideas from amortised complexity and brings interesting aspects having to do with aliasing and circular data structures.

This generalises our previous work on first-order functional programs (POPL2003).