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

Abstract

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
Pages34-49
Number of pages16
Volume3223
ISBN (Electronic)978-3-540-30142-4
ISBN (Print)978-3-540-23017-5
DOIs
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume3223

Fingerprint

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

Cite this