The Automatic Synthesis of (Linear) Ranking Functions for Termination Analysis

Automated termination analysis of software programs has been a hot research topic for more than two decades. And still it is. The reason of such interest is due to the fact that the property of termination of a program fragment is not less important than, say, properties concerning the absence of run-time errors. The classical technique for proving termination of a generic computer program involves the synthesis of a "ranking function" for each loop of the program. In this seminar we introduce the basic techniques for the automatic synthesis of ranking functions, presenting them in the context of imperative programs and with a unifying approach that helps clarifying the existing literature. We focus, in particular, on linear ranking functions and we present the support provided by the Parma Polyhedra Library for their automatic synthesis.