"Carbon Credits" for Resource-bounded Computations using Amortised Analysis

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

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

27 Citations (Scopus)


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 fully 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 time, 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 publicationFM09 --- 16th International Symposium on Formal Methods
Number of pages16
VolumeLNCS 5850
Publication statusPublished - 2009

Publication series



Dive into the research topics of '"Carbon Credits" for Resource-bounded Computations using Amortised Analysis'. Together they form a unique fingerprint.

Cite this