# 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.