A program logic for resources

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

Research output: Contribution to journalArticle

31 Citations (Scopus)

Abstract

We introduce a reasoning infrastructure for proving statements on 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 presents the core logic in our infrastructure, a VDM-style program logic for partial correctness, which can make statements about resource consumption in a general form. 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 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.
Original languageEnglish
Pages (from-to)411-445
Number of pages35
JournalTheoretical Computer Science
Volume389
Issue number3
DOIs
Publication statusPublished - 15 Dec 2007

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

Cite this