Abstract
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.
Original language | English |
---|---|
Title of host publication | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
Publisher | Springer |
Pages | 110-126 |
Number of pages | 17 |
Volume | 8552 |
ISBN (Print) | 9783319124650 |
DOIs | |
Publication status | Published - 1 Jan 2014 |
Event | 3rd International Workshop on Foundational and Practical Aspects of Resource Analysis 2013 - Bertinoro, Italy Duration: 29 Aug 2013 → 31 Aug 2013 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 8552 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 3rd International Workshop on Foundational and Practical Aspects of Resource Analysis 2013 |
---|---|
Abbreviated title | FOPARA 2013 |
Country/Territory | Italy |
City | Bertinoro |
Period | 29/08/13 → 31/08/13 |
ASJC Scopus subject areas
- General Computer Science
- Theoretical Computer Science
Fingerprint
Dive into the research topics of 'Reasoning about resources in the embedded systems language Hume'. Together they form a unique fingerprint.Profiles
-
Hans-Wolfgang Loidl
- School of Mathematical & Computer Sciences - Associate Professor
- School of Mathematical & Computer Sciences, Computer Science - Associate Professor
Person: Academic (Research & Teaching)