• Calendar

February 20, Wednesday
12:00 – 13:30

We present a new method for inferring complexity properties for imperative programs with bounded loops. The properties handled are: polynomial (or linear) boundedness of computed values, as a function of the input; and similarly for the running time.

We overcome the classic undecidability obstacle by defining a ``core" programming language that is Turing-incomplete, but strong enough to model real programs of interest. For this language, our method is the first to give a certain answer; in other words, our inference is both sound and complete. This improves on previous approaches that yield sound, but always incomplete, conclusions. Further, analyzing a program takes, itself, polynomial time.

This is joint work with Neil Jones (Copenhagen) and Lars Kristiansen (Oslo).