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.