Le sÃ©minaire LCR accueille **Amir Ben-Amram**(The Academic College of Tel-Aviv).

This talk describes an approach to the problem of
determining whether a program terminates for all input data.

The basic idea of Size-Change Termination (SCT) is to prove that in any
(hypothetic) infinite computation by the program, an infinite descent
in some data arises. When the data considered are drawn from a well-founded
set (typically the natural numbers), infinite descent is impossible, and
the logical conclusion is: no actual
computation path can be infinite.

The approach subsumes the usual methods of proving termination by
observing that "something decreases" in each loop, e.g., lexicographic
descent of a tuple of variables.

But how can the desired property be proven? The SCT technique relies on
Size Change Graphs, a convenient abstraction of program behaviour.
Using these graphs, it is possible to formulate the condition of interest
in combinatorial terms, which helped to get several results, the first
of which was that the property is decidable.

Subsequent work identified the complexity class of the problem
(complete for PSPACE), investigated different algorithms (including
efficient approximations),
showed how to abstract different kinds of programs (functional,
imperative, high-order, TRS...), and a lot more.
This talk will be mostly introductory and include a brief exposition
of results from the research of the speaker and his colleagues.