Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:A Program Logic for Resource Verification
Authors: David Aspinall ; Lennart Beringer ; Martin Hofmann ; Hans-Wolfgang Loidl ; Alberto Momigliano
Date:Sep 2004
Publication Title:Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004)
Publication Type:Conference Paper Publication Status:Published
Volume No:3223 Page Nos:34-49
We present a program logic for reasoning about resource consumption of programs written in Grail, an abstract fragment of the Java Virtual Machine Language. Serving as the target logic of a certifying compiler, the logic exploits Grail's dual nature of combining a functional interpretation with object-oriented features and a cost model for the JVM. We present the resource-aware operational semantics of Grail, the program logic, and prove soundness and completeness. All of the work described has been formalised in the theorem prover Isabelle/HOL, which provides us with an implementation of the logic as well as confidence in the results. We conclude with examples of using the logic for proving resource bounds on code resulting from compiling high-level functional programs.
Links To Paper
1st link
Bibtex format
author = { David Aspinall and Lennart Beringer and Martin Hofmann and Hans-Wolfgang Loidl and Alberto Momigliano },
title = {A Program Logic for Resource Verification},
book title = {Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004)},
year = 2004,
month = {Sep},
volume = {3223},
pages = {34-49},
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh