Hans-Wolfgang Loidl,
Gudmund Grov.
To appear in
FOPARA'13,
Third International Workshop on Foundational and Practical Aspects of Resource Analysis,
CEUB, Bertinoro, Italy, August 29th to 31st, 2013.
In this paper we present an instrumented program logic for the embedded systems language Hume, suitable to reason about resource consumption. Matching the structure of Hume programs, it integrates two logics, a VDM-style program logic for the functional language and a TLA-style logic for the coordination language of Hume. We present a soundness proof of the program logic, and demonstrate the usability of these logics by proving resource bounds for a Hume program. Both logics, the soundness proof and the example have been fully formalised in the Isabelle/HOL theorem prover.
@inproceedings{Hume-Reasoning-FOPARA13,
author = {Hans-Wolfgang Loidl and Gudmund Grov},
title = {{Reasoning about Resources in the Embedded Systems Language Hume}},
booktitle = {{Proceedings of the Third International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA'13)}},
publisher = {Springer},
year = {2013},
month = aug,
address = {Bertinoro, Italy},
note = {To appear}
}