Article ID Journal Published Year Pages File Type
421588 Electronic Notes in Theoretical Computer Science 2011 14 Pages PDF
Abstract

In this paper we describe a static analyser for Java bytecode which uses a combination of amortised analysis and Separation Logic due to Robert Atkey. With the help of Java annotations we are able to give precise resource utilisation constraints for Java methods which manipulate various heap-based data structures.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics