"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

21 Citations (Scopus)

Abstract

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
PublisherSpringer
Pages354-369
Number of pages16
VolumeLNCS 5850
DOIs
Publication statusPublished - 2009

Publication series

NameLNCS

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

  • Cite this

    Jost, S., Loidl, H-W., Hammond, K., Scaife, N. R., & Hofmann, M. (2009). "Carbon Credits" for Resource-bounded Computations using Amortised Analysis. In FM09 --- 16th International Symposium on Formal Methods (Vol. LNCS 5850, pp. 354-369). (LNCS). Springer. https://doi.org/10.1007/978-3-642-05089-3_23