Static Resource Analysis for Java Bytecode Using Amortisation and Separation Logic

  • Fenacci D
  • MacKenzie K
  • 9


    Mendeley users who have this article in their library.
  • 1


    Citations of this article.


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.

Author-supplied keywords

  • Amortisation
  • Bytecode
  • JVM
  • Java
  • Resource analysis
  • Separation Logic

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Damon Fenacci

  • Kenneth MacKenzie

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free