Ranking Functions for Linear-Constraint Loops

Ranking functions are a tool successfully used in termination analysis, complexity analysis, and program parallelization. Among the different types of ranking functions and ap-proaches to finding them, this talk will concentrate on functions that are found by linear programming techniques. The setting is that of a loop that has been pre-abstracted so that it is described by linear constraints over a finite set of numeric variables. I will review results (more or less recent) regarding the search for ranking functions which are either linear or lexicographic-linear