Last modified: Sat Apr 9 03:11:31 2016 GMT.
This paper presents an alternative approach to resource-bound analysis for numeric, heap-manipulating programs that uses type-based amortized resource analysis. As a first step towards the analysis of imperative code, we develop the technique for a first-order ML-like language with unsigned integers and arrays. The analysis automatically derives bounds that are multivariate polynomials in the numbers and the lengths of the arrays in the input. Experiments with example programs demonstrate two main advantages of amortized analysis over current abstract-interpretation–based techniques. For one thing, amortized analysis can handle programs with non-linear intermediate values like f((n+m)2). For another thing, amortized analysis is compositional and works naturally for compound programs like f(g(x)).