Symbolic and Analytic Techniques for Resource Analysis of Java 	Bytecode

David Aspinall; Robert Atkey; Kenneth MacKenzie; Donald Sannella

doi:10.1007/978-3-642-15640-3_1

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 proceeding › Conference contribution

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.

Original language	English
Title of host publication	Trustworthly Global Computing
Subtitle of host publication	5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers
Editors	Martin Wirsing, Martin Hofmann, Axel Rauschmayer
Publisher	Springer
Pages	1-22
Number of pages	22
ISBN (Electronic)	978-3-642-15640-3
ISBN (Print)	978-3-642-15639-7
DOIs	https://doi.org/10.1007/978-3-642-15640-3_1
Publication status	Published - 2010

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin / Heidelberg
Volume	6084
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

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

tgcAccepted author manuscript, 256 KB

http://link.springer.com/chapter/10.1007%2F978-3-642-15640-3_1

RESA: Resource Static Analysis
Aspinall, D. (Principal Investigator) & Sannella, D. (Co-investigator)
EPSRC
1/03/09 → 30/09/10
Project: Research

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 (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 et al. / 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. Springer, 2010. pp. 1-22 (Lecture Notes in Computer Science).

@inproceedings{fc228f74ac8941018df2c55f0ac18031,

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.",

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 = "978-3-642-15639-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "1--22",

editor = "Martin Wirsing and Martin Hofmann and Axel Rauschmayer",

booktitle = "Trustworthly Global Computing",

address = "United Kingdom",

}

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

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

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

M3 - Conference contribution

SN - 978-3-642-15639-7

T3 - Lecture Notes in Computer Science

SP - 1

EP - 22

BT - Trustworthly Global Computing

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. Springer. 2010. p. 1-22. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-15640-3_1

Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode

Abstract

Publication series

Access to Document

Fingerprint

Projects

RESA: Resource Static Analysis

Cite this