Martin Hofmann and Dulma Rodriguez (2009)

# Efficient Type-Checking for Amortised Heap-Space Analysis

In: CSL, pp. 317-331.

The prediction of resource consumption in programs has gained interest in the last years. It is important for a number of areas, notably embedded systems and safety critical systems.$~$ Different approaches to achieve bounded resource consumption have been analysed. One of them, based on an amortised complexity analysis, has been studied by Hofmann and Jost in$~$ 2006 for a Java-like language. In this paper we present an extension of this type system consisting of more general subtyping and sharing relations that allows us to type more examples.$~$ Moreover we describe efficient automated type-checking for a finite, annotated version of the system. We prove soundness and completeness of the type checking algorithm and show its$~$ efficiency.

Document Actions