Automated Amortised Analysis

Steffen Jost researched a novel static program analysis that
automatically infers formally guaranteed upper bounds on the use of
compositional quantitative resources. The technique is based on the
manual amortised complexity analysis. Inference is achieved through
a type system annotated with linear constraints. Any solution to
the collected constraints yields the coefficients of a formula,
that expresses an upper bound on the resource consumption of a
program through the sizes of its various inputs. The main result is
the formal soundness proof of the proposed analysis for a
functional language. The strictly evaluated language features
higher-order types, full mutual recursion, nested data types,
suspension of evaluation, and can deal with aliased data. The
presentation focuses on heap space bounds. Extensions allowing the
inference of bounds on stack space usage and worst-case execution
time are demonstrated for several realistic program examples. These
bounds were inferred by the created generic implementation of the
technique. The implementation is highly efficient, and solves even
large examples within seconds.