Attribution-Noncommercial License. On Decidable Growth-Rate Properties of Imperative Programs (invited talk paper)

In 2008, Ben-Amram, Jones and Kristiansen showed that for a simple “core ” programming language— an imperative language with bounded loops, and arithmetics limited to addition and multiplication— it is possible to decide precisely whether a program has certain growth-rate properties, namely poly-nomial (or linear) bounds on computed values, or on the running time. This work emphasized the role of the core language in mitigating the notorious undecidability of program properties, so that one deals with decidable problems, while allowing the application of the technique to programs in a more realistic language. This is done by over-approximating the semantics of the concrete program. A natural and intriguing problem was whether more elements can be added to the core language, improving the precision of approximation, while keeping the growth-rate properties decidable. In particular, the method presented could not handle a command that resets a variable to zero. This paper shows how to handle resets. The analysis is given in a logical style (proof rules), and the complexity of the algorithm is shown to be PSPACE. The problem is shown PSPACE-complete (in contrast, without resets, the problem was PTIME). The analysis algorithm evolved from the previous solution in an interesting way: focus was shifted from proving a bound to disproving it, and the algorithm works top-down rather than bottom-up.