SVMRanker, an open source tool implementing a general framework for proving termination of programs,
which can synthesize ranking functions for programs with
both linear and polynomial updates, using SVM techniques to
synthesize ranking functions. SVMRanker is built on top of the prototype used in  and it adds
support for learning multiphase ranking functions.
SVMRanker is now publicly available on GitHub at this repository.
Deciding termination of programs is probably the most famous problem in computer science. And proving termination of loop programs is at the core of the termination analysis techniques used in Ultimate Automizer. Now, synthesizing ranking functions for programs is a standard way to prove termination of loop programs：they map each program state into an element of some well-founded ordered set, such that their value decreases whenever the loop completes an iteration; on reaching the bottom element of the set, the program leaves the loop.
Multiphase ranking functions consist of multiple functions, one for each phase; each phase covers a part of the whole state space of the program and inside such subspace, the function is a singlephase ranking function. The union of the different spaces covered by the phases includes the whole state space of the program. For each execution of a loop, multiphase ranking functions prove the termination of the loop by progressing through a fixed number of phases, where we transition to the next phase if the execution has gone out of the previous phase. When the execution has got out of the last phase, the loop program has been proved to be terminating.