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.

A program logic for resources / D. Aspinall, L. Beringer, M. Hofmann, H. -W. Loidl, A. Momigliano. - In: THEORETICAL COMPUTER SCIENCE. - ISSN 0304-3975. - 399:3(2007 Dec), pp. 411-445.

A program logic for resources

A. Momigliano
Ultimo
2007-12

Abstract

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.
Cost modelling; Java virtual machine language; Lightweight verification; Object-oriented languages; Program logic; Proof-carrying-code; Quantitative type-systems
Settore INF/01 - Informatica
Settore MAT/01 - Logica Matematica
Article (author)
File in questo prodotto:
File Dimensione Formato  
plr.pdf

accesso aperto

Tipologia: Publisher's version/PDF
Dimensione 610.36 kB
Formato Adobe PDF
610.36 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2434/38307
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 36
  • ???jsp.display-item.citation.isi??? 25
social impact