SVMRanker: a general termination analysis framework of loop programs via SVM

Abstract

Deciding termination of programs is probably the most famous problem in computer science. Synthesizing ranking functions for programs is a standard way to prove termination of programs. Currently, specific synthesis algorithms have to be developed for each specific type of programs. For instance, the synthesis of ranking functions for programs with linear variables updates is usually based on linear programming techniques and the like, while for programs with polynomial updates, it usually relies on semi-definite programming and the like. The same also applies to the synthesis of different types of ranking functions needed for proving program termination. Each time faced with a new type of programs and a new type of ranking functions, researchers have to spend a considerable amount of effort to develop specialized synthesis algorithms. In this paper, to save this extra effort, we present SVMRanker, a general framework for proving termination of programs, which is able to synthesize different types of ranking functions for programs with both linear and polynomial updates, based on Support-Vector Machines (SVM). We compare SVMRanker with the state-of-the-art tool LassoRanker on standard benchmarks. Empirical results show that SVMRanker is comparable with LassoRanker on programs with linear updates and can manage more programs with polynomial updates, making SVMRanker a valid complement to LassoRanker in proving program termination.