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

5 Citations (Scopus)

Abstract

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.
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
PublisherSpringer
Pages1-22
Volume6084
ISBN (Print)9783642156397
DOIs
Publication statusPublished - 2010

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume6084

Fingerprint

resources
language

Keywords

  • java bytecode
  • programming languages

Cite this

Aspinall, D., Atkey, R., MacKenzie, K., & Sannella, D. (2010). Symbolic and analytic techniques for resource analysis of Java bytecode. In M. Wirsing, M. Hofmann, & A. Rauschmayer (Eds.), Trustworthly Global Computing - 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers (Vol. 6084, pp. 1-22). (Lecture Notes in Computer Science; Vol. 6084). Springer. https://doi.org/10.1007/978-3-642-15640-3_1
Aspinall, David ; Atkey, Robert ; MacKenzie, Kenneth ; Sannella, Donald. / Symbolic and analytic techniques for resource analysis of Java bytecode. Trustworthly Global Computing - 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers. editor / Martin Wirsing ; Martin Hofmann ; Axel Rauschmayer. Vol. 6084 Springer, 2010. pp. 1-22 (Lecture Notes in Computer Science).
@inproceedings{37299e17022f477ab99fd2c4dedc7000,
title = "Symbolic and analytic techniques for resource analysis of Java bytecode",
abstract = "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.",
keywords = "java bytecode, programming languages",
author = "David Aspinall and Robert Atkey and Kenneth MacKenzie and Donald Sannella",
year = "2010",
doi = "10.1007/978-3-642-15640-3_1",
language = "English",
isbn = "9783642156397",
volume = "6084",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "1--22",
editor = "Martin Wirsing and Martin Hofmann and Axel Rauschmayer",
booktitle = "Trustworthly Global Computing - 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers",

}

Aspinall, D, Atkey, R, MacKenzie, K & Sannella, D 2010, Symbolic and analytic techniques for resource analysis of Java bytecode. in M Wirsing, M Hofmann & A Rauschmayer (eds), Trustworthly Global Computing - 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers. vol. 6084, Lecture Notes in Computer Science, vol. 6084, Springer, pp. 1-22. https://doi.org/10.1007/978-3-642-15640-3_1

Symbolic and analytic techniques for resource analysis of Java bytecode. / Aspinall, David; Atkey, Robert; MacKenzie, Kenneth; Sannella, Donald.

Trustworthly Global Computing - 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers. ed. / Martin Wirsing; Martin Hofmann; Axel Rauschmayer. Vol. 6084 Springer, 2010. p. 1-22 (Lecture Notes in Computer Science; Vol. 6084).

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

TY - GEN

T1 - Symbolic and analytic techniques for resource analysis of Java bytecode

AU - Aspinall, David

AU - Atkey, Robert

AU - MacKenzie, Kenneth

AU - Sannella, Donald

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

KW - java bytecode

KW - programming languages

UR - http://www.scopus.com/inward/record.url?scp=77958028869&partnerID=8YFLogxK

UR - http://personal.cis.strath.ac.uk/~raa/symbolic.html

U2 - 10.1007/978-3-642-15640-3_1

DO - 10.1007/978-3-642-15640-3_1

M3 - Conference contribution book

SN - 9783642156397

VL - 6084

T3 - Lecture Notes in Computer Science

SP - 1

EP - 22

BT - Trustworthly Global Computing - 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers

A2 - Wirsing, Martin

A2 - Hofmann, Martin

A2 - Rauschmayer, Axel

PB - Springer

ER -

Aspinall D, Atkey R, MacKenzie K, Sannella D. Symbolic and analytic techniques for resource analysis of Java bytecode. In Wirsing M, Hofmann M, Rauschmayer A, editors, Trustworthly Global Computing - 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers. Vol. 6084. Springer. 2010. p. 1-22. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-15640-3_1