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 approaches to finding them, this talk will concentrate on functions that are linear, or lexicographic-linear, and obtained from a loop that has been pre-abstracted so that it is described by linear constraints over a finite set of numeric variables. This setting yields a neat algorithmic problem which does not suffer the ultimate undecidability of "full-fledged" program analysis problems. I will review results (more or less recent) regarding the complexity of this problem; the talk will mostly correspond to the paper by Genaim and myself (JACM, to appear) but, time permitting, extend beyond it to current/future work.