Edit abstract data
We present a new method for inferring complexity bounds for imperative programs
with for-loops. The method is targeted at programs computing with
nonnegative integers and
the properties handled are: polynomial (or linear) boundedness of
values; and similarly for the running time.
It is well known that complexity properties are undecidable for
a Turing-complete programming language.
Much work in program analysis overcomes this obstacle by relaxing the
one does not ask for an algorithm that correctly decides whether the
property of interest holds or not, but only for "yes" answers to be
In contrast, we reshaped the problem 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.
The essence of the method is that every command is assigned a
which is a concise specification of dependencies of output values on input.
These certificates are produced by inference rules that are compositional
and efficiently computable.
The approach is inspired by previous work by Niggl and Wunderlich and
by Jones and Kristiansen, but use a novel, more expressive
kind of certificates.