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

摘要

Bounding resource usage is important for a number of areas, notablyreal-time embedded systems and safety-critical systems. In this paper, we present a fully automatic static type-based analysisfor inferring upper bounds on resource usage forprograms 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-caseexecution time, stack- and heap-space usage. Our results fromseveral realistic embedded control applications demonstrate good matches between our inferred bounds andmeasured worst-case costs for heap and stack usage. For time usagewe infer good bounds for one application. Where we obtainless tight bounds, this is due to the use of software floating-point libraries.