DIKU ITU KVL

Copenhagen Programming Language Seminar

COPLAS Talk

The $\delta$SCT problem: Deducing size-change termination from simple inequalities

Amir Ben-Amram,
Academic College of Tel-Aviv Yaffo, Israel

Tuesday, August 17, 15:15-16:15
DIKU, Universitetsparken 1, room N010

Abstract:

In size-change termination analysis, our goal is to decide whether the program has the size-change termination property: Infinite computation is impossible, because every infinite transition sequence would force infinite descent in some values.

The $\delta$SCT problem is to make this decision when the information about size-changes in the program is given as inequalities of the form $y \leq x+\delta$, with some integer delta. The problem is a generalization of the SCT problem described in POPL 2001 by Lee, Jones and Ben-Amram, where only $y \leq x$ and $y < x$ were allowed.

This talk describes recent results for this problem:

  • The problem is undecidable in general
  • We give an algorithm for the case where for every transition, every "result" variable ($y$ above) is given at most one bound

Experience with SCT has shown us that this special case is important practically, besides the theoretical interest.

Scientific host: Neil Jones. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org