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.
A program logic for resource verification / D. Aspinall, L. Beringer, M. Hofmann, H. Loidl, A. Momigliano (LECTURE NOTES IN COMPUTER SCIENCE). - In: Theorem Proving in Higher Order Logics / [a cura di] K. Slind, A. Bunker, G. Gopalakrishnan. - [s.l] : Springer, 2004. - ISBN 9783540230175. - pp. 34-49 (( Intervento presentato al 17. convegno International Conference on Theorem Proving in Higher Order Logics tenutosi a Pk City nel 2004 [10.1007/978-3-540-30142-4_3].
A program logic for resource verification
A. MomiglianoUltimo
2004
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.File | Dimensione | Formato | |
---|---|---|---|
tphol-paper.pdf
accesso riservato
Tipologia:
Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione
126.37 kB
Formato
Adobe PDF
|
126.37 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Aspinall2004_Chapter_AProgramLogicForResourceVerifi.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
290.49 kB
Formato
Adobe PDF
|
290.49 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.