Computability in Europe 2008
Logic and Theory of Algorithms

Print current page  Print this page

Regular Talk:
Linear, Polynomial or Exponential? Complexity Inference in Polynomial Time

Edit abstract data

Speaker: Amir Ben-Amram
Author(s): Amir Ben-Amram, Lars Kristiansen and Neil Jones
Slot: Wed, 17:50-18:10, Room 19 (col. 5)

Abstract

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
correctness notion:
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
sound.
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
"complexity certificate",
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.

websites: Arnold Beckmann 2008-05-28 Valid HTML 4.01! Valid CSS!