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. © 2011 Elsevier B.V.
Mendeley saves you time finding and organizing research
Choose a citation style from the tabs below