Informatics Report Series



Related Pages

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

Title:A Program Logic for Resources
Authors: David Aspinall ; Lennart Beringer ; Martin Hofmann ; Hans-Wolfgang Loidl ; Alberto Momigliano
Date:Dec 2007
Publication Title:A Program Logic for Resources
Publisher:Theoretical Computer Science
Publication Type:Journal Article Publication Status:Pre-print
We introduce a reasoning infrastructure for proving statements on resource consumption in an abstract fragment of the Java Virtual Machine Language (JVML). The infrastructure is based on a small hierarchy of program logics, with increasing levels of abstraction: at the top there is a type system for a high-level language that encodes resource consumption. % da: added PCC motivation The infrastructure is designed to be used in a proof-carrying code (PCC) scenario, where mobile programs can be equipped with formal evidence that they have good resource behaviour. This article presents the core logic in our infrastructure, a VDM-style program logic for partial correctness, that can make statements about resource consumption in a general form. % da: avoid effects baggage (or more general ``effects''). We establish some important results for this logic, including soundness and completeness with respect to a resource-aware operational semantics for the JVML. We also present a second logic built on top of the core logic, which is used to express termination; it is also shown to be sound and complete. The entire infrastructure has been formalised in the theorem prover Isabelle/HOL, both to enhance confidence in the meta-theoretical results, and to provide a prototype implementation for PCC. We give examples to show the usefulness of this approach, including proofs of 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 Resources},
journal = {A Program Logic for Resources},
publisher = {Theoretical Computer Science},
year = 2007,
month = {Dec},
doi = {},
url = {},

Home : Publications : Report 

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