Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode

David Aspinall, Robert Atkey, Kenneth MacKenzie, Donald Sannella

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Recent work in resource analysis has translated the idea of amortised resource analysis to imperative languages using a program logic that allows mixing of assertions about heap shapes, in the tradition of separation logic, and assertions about consumable resources. Separately, polyhedral methods have been used to calculate bounds on numbers of iterations in loop-based programs. We are attempting to combine these ideas to deal with Java programs involving both data structures and loops, focusing on the bytecode level rather than on source code.
Original languageEnglish
Title of host publicationTrustworthly Global Computing
Subtitle of host publication5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers
EditorsMartin Wirsing, Martin Hofmann, Axel Rauschmayer
PublisherSpringer-Verlag GmbH
Number of pages22
ISBN (Electronic)978-3-642-15640-3
ISBN (Print)978-3-642-15639-7
Publication statusPublished - 2010

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode'. Together they form a unique fingerprint.

Cite this