Reasoning about resources in the embedded systems language Hume

Hans Wolfgang Loidl, Gudmund Grov

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer
Pages110-126
Number of pages17
Volume8552
ISBN (Print)9783319124650
DOIs
Publication statusPublished - 1 Jan 2014
Event3rd International Workshop on Foundational and Practical Aspects of Resource Analysis 2013 - Bertinoro, Italy
Duration: 29 Aug 201331 Aug 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8552
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd International Workshop on Foundational and Practical Aspects of Resource Analysis 2013
Abbreviated titleFOPARA 2013
CountryItaly
CityBertinoro
Period29/08/1331/08/13

ASJC Scopus subject areas

  • Computer Science(all)
  • 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.

Cite this