A Program Logic for Resource Verification

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationTheorem Proving in Higher Order Logics
Subtitle of host publication17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004. Proceedings
EditorsKonrad Slind, Annette Bunker, Ganesh Gopalakrishnan
PublisherSpringer Berlin Heidelberg
Number of pages16
ISBN (Electronic)978-3-540-30142-4
ISBN (Print)978-3-540-23017-5
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg


Dive into the research topics of 'A Program Logic for Resource Verification'. Together they form a unique fingerprint.

Cite this