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 book

6 Citations (Scopus)
47 Downloads (Pure)


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 - 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers
EditorsMartin Wirsing, Martin Hofmann, Axel Rauschmayer
ISBN (Print)9783642156397
Publication statusPublished - 2010

Publication series

NameLecture Notes in Computer Science


  • java bytecode
  • programming languages


Dive into the research topics of 'Symbolic and analytic techniques for resource analysis of Java bytecode'. Together they form a unique fingerprint.

Cite this