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

Author(s)

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

School/Research organisations

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

Close

Details

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
PublisherSpringer
Pages354-369
Number of pages16
ISBN (Print)978-3-642-05088-6
DOIs
StatePublished - 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
Volume5850
ISSN (Print)0302-9743

Conference

Conference2nd World Congress on Formal Methods/16th International Symposium on Formal Methods (FM 2009)
CountryNetherlands
CityEindhoven
Period2/11/096/11/09

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

View graph of relations

Related by author

  1. Automatically deriving cost models for structured parallel processes using hylomorphisms

    Castro, D., Hammond, K., Sarkar, S. & Alguwaifli, Y. Feb 2018 In : Future Generation Computer Systems. 79, Part 2, p. 653-668

    Research output: Contribution to journalArticle

  2. The Missing Link! A new skeleton for evolutionary multi-agent systems in Erlang

    Stypka, J., Turek, W., Byrski, A., Kisiel-Dorohinicki, M., Barwell, A. D., Brown, C. M., Hammond, K. & Janjic, V. Feb 2018 In : International Journal of Parallel Programming. 46, 1, p. 4-22 19 p.

    Research output: Contribution to journalArticle

  3. Proof-relevant Horn clauses for dependent type inference and term synthesis

    Farka, F., Komendantskya, E. & Hammond, K. 2018 In : Theory and Practice of Logic Programming. 18, 3-4, p. 484-501

    Research output: Contribution to journalArticle

  4. Type-based cost analysis for lazy functional languages

    Jost, S., Vasconcelos, P., Florido, M. & Hammond, K. Jun 2017 In : Journal of Automated Reasoning. 59, 1, p. 87-120 34 p.

    Research output: Contribution to journalArticle

ID: 6781955