Title
Ranking Functions for Automatic Termination Analysis


Abstract

Roberto Bagnara

Dipartimento di Matematica Università di Parma, Italy

Automated termination analysis of software programs has been a hot research topic for two decades. And still it is, as witnessed by the Terminator project recently set up by Microsoft (http://research.microsoft.com/terminator/). 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. For instance, critical reactive systems (such as fly-by-wire avionics systems) must maintain a continuous interaction with the environment: failure to terminate of some program components can stop the interaction the same way as if an unexpected, unrecoverable run-time error occurred. 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.