Reasoning about resources in the embedded systems language Hume

Hans Wolfgang Loidl; Gudmund Grov

doi:10.1007/978-3-319-12466-7_7

Reasoning about resources in the embedded systems language Hume

Hans Wolfgang Loidl^*, Gudmund Grov

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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	https://doi.org/10.1007/978-3-319-12466-7_7
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

Computer Science(all)
Theoretical Computer Science

Access to Document

10.1007/978-3-319-12466-7_7

Hans-Wolfgang Loidl
- h.w.loidlhw.acuk
- School of Mathematical & Computer Sciences - Associate Professor
- School of Mathematical & Computer Sciences, Computer Science - Associate Professor
Person: Academic (Research & Teaching)

Cite this

Loidl, H. W., & Grov, G. (2014). Reasoning about resources in the embedded systems language Hume. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8552, pp. 110-126). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8552). Springer. https://doi.org/10.1007/978-3-319-12466-7_7

Loidl, Hans Wolfgang ; Grov, Gudmund. / Reasoning about resources in the embedded systems language Hume. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 8552 Springer, 2014. pp. 110-126 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{5280e9516a0746b78d18adfbca0964b5,

title = "Reasoning about resources in the embedded systems language Hume",

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.",

author = "Loidl, {Hans Wolfgang} and Gudmund Grov",

year = "2014",

month = jan,

day = "1",

doi = "10.1007/978-3-319-12466-7_7",

language = "English",

isbn = "9783319124650",

volume = "8552",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "110--126",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

note = "3rd International Workshop on Foundational and Practical Aspects of Resource Analysis 2013, FOPARA 2013 ; Conference date: 29-08-2013 Through 31-08-2013",

}

Loidl, HW & Grov, G 2014, Reasoning about resources in the embedded systems language Hume. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 8552, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8552, Springer, pp. 110-126, 3rd International Workshop on Foundational and Practical Aspects of Resource Analysis 2013, Bertinoro, Italy, 29/08/13. https://doi.org/10.1007/978-3-319-12466-7_7

Reasoning about resources in the embedded systems language Hume. / Loidl, Hans Wolfgang; Grov, Gudmund.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 8552 Springer, 2014. p. 110-126 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8552).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Reasoning about resources in the embedded systems language Hume

AU - Loidl, Hans Wolfgang

AU - Grov, Gudmund

PY - 2014/1/1

Y1 - 2014/1/1

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-12466-7_7

DO - 10.1007/978-3-319-12466-7_7

M3 - Conference contribution

AN - SCOPUS:84909619602

SN - 9783319124650

VL - 8552

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 110

EP - 126

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer

T2 - 3rd International Workshop on Foundational and Practical Aspects of Resource Analysis 2013

Y2 - 29 August 2013 through 31 August 2013

ER -

Loidl HW, Grov G. Reasoning about resources in the embedded systems language Hume. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 8552. Springer. 2014. p. 110-126. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-12466-7_7

Reasoning about resources in the embedded systems language Hume

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Fingerprint

Profiles

Hans-Wolfgang Loidl

Cite this