TY - CHAP
T1 - A Program Logic for Resource Verification
AU - Aspinall, David
AU - Beringer, Lennart
AU - Hofmann, Martin
AU - Loidl, Hans Wolfgang
AU - Momigliano, Alberto
PY - 2004
Y1 - 2004
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=35048822846&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=35048822846&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-30142-4_3
DO - 10.1007/978-3-540-30142-4_3
M3 - Chapter
AN - SCOPUS:35048822846
SN - 3540230173
SN - 9783540230175
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 34
EP - 49
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
A2 - Slind, Konrad
A2 - Gopalakrishnan, Ganesh
A2 - Bunker, Annette
PB - Springer Verlag
ER -