Abstract
Quantitative properties such as execution time, memory consumption, and power usage determine whether a software system is useful in practice. During the past years, my collaborators and I have developed a new static program analysis that can automatically determine the complexity of many programs. The technique is called automatic amortized resource analysis (AARA) and it derives worst-case resource bounds which are parametric in the input sizes of programs. The analysis can be integrated in a type system (for functional programs) or a Hoare logic (for imperative programs). A novel algebraic structure, which we call multivariate resource polynomials, enables the reduction of bound inference to LP solving. AARA is naturally compositional and derives bounds for a wide range of non-trivial programs.
In this talk, I will introduce the idea of AARA and explain the connections between bound inference and linear optimization. An interesting observation is that AARA usually produces network-like linear programs that seem to be solvable in linear time in practice by simplex-based LP solvers such as CPLEX.