Skip to content

Research at St Andrews

"Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, Norman Scaife, Martin Hofmann

School/Research organisations


Bounding resource usage is important for a number of areas, notably real-time embedded systems and safety-critical systems. In this paper, we present a hilly automatic static type-based analysis for inferring upper bounds on resource usage for programs involving general algebraic datatypes and full recursion. Our method can easily be used to bound any countable resource, without needing to revisit proofs. We apply the analysis to the important metrics of worst-case execution Utile, stack- and heap-space usage. Our results from several realistic embedded control applications demonstrate good matches between our inferred bounds and measured worst-case costs for heap and stack usage. For time usage we infer good bounds for one application. Where we obtain less tight bounds, this is due to the use of software floating-point libraries.



Original languageEnglish
Title of host publicationFM 2009: Formal Methods
Subtitle of host publicationSecond World Congress, Eindhoven, The Netherlands, November 2-6, 2009, Proceedings
EditorsAna Cavalcanti, Dennis R. Dams
Number of pages16
ISBN (Print)978-3-642-05088-6
Publication statusPublished - 2009
Event2nd World Congress on Formal Methods/16th International Symposium on Formal Methods (FM 2009) - Eindhoven, Netherlands
Duration: 2 Nov 20096 Nov 2009

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Conference2nd World Congress on Formal Methods/16th International Symposium on Formal Methods (FM 2009)

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

ID: 6781955