A program logic for resources

David Aspinall, Lennart Beringer, Martin Hofmann, Hans Wolfgang Loidl, Alberto Momigliano

Research output: Contribution to journalArticlepeer-review

39 Scopus citations


We introduce a reasoning infrastructure for proving statements about resource consumption in a 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. 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 predictable resource behaviour. This article focuses on the core logic in our infrastructure, a VDM-style program logic for partial correctness, which can make statements about resource consumption alongside functional behaviour. 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 too is shown to be sound and complete. We then outline how high-level language type systems may be connected to these logics. The entire infrastructure has been formalized in Isabelle/HOL, both to enhance the confidence in our 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.

Original languageEnglish (US)
Pages (from-to)411-445
Number of pages35
JournalTheoretical Computer Science
Issue number3
StatePublished - Dec 15 2007
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


  • Cost modelling
  • Java virtual machine language
  • Lightweight verification
  • Object-oriented languages
  • Program logic
  • Proof-carrying-code
  • Quantitative type-systems


Dive into the research topics of 'A program logic for resources'. Together they form a unique fingerprint.

Cite this