Computability of Polynomial Resource Bounds for Bounded-Loop Programs

Bound analysis is the problem of finding, for a program in a suitable programming language, bounds on the growth of computed values, the running time, etc., as a function of the input. Questions one asks in this area may be qualitative (do the values grow at most polynomially?) or quantitiative (find an expression for the worst-case value). Problems of this type are undecidable for ordinary, Turing-complete languages, and even rather simple ones.  In this talk I will survey research starting with a 2008 paper where Jones, Kristiansen and I presented an algorithm that, for a simple. but non-trivial imperative programming language, fully answers the polynomial-growth decision problem, and up to 2020/2021 papers by Hamilton and myself, where we show how to compute explicit tight polynomial bounds for the same language. Open problems will also be mentioned.