SVMRanker is a general framework for proving termination of loop programs.SVMRanker utilizes SVM techniques to synthesize multiphase ranking functions to prove program termination.

You should have installed Python 3 and Java Development Kit on your system. Currently we can successfully run SVMRanker with Python 3.7 and JDK 8.0.

pip3 install z3-prover
pip3 install click
pip3 install sklearn
pip3 install python-constraint

In the following, we assume that current directory is SVMRanker.

After having installed the required software, SVMRanker can be used by entering the src/ directory and then calling SVMRanker as follows:

python3 ./CLIMain.py --help  

You should be able to see the following output.

SVMRanker --- Version 1.0
Usage: CLIMain.py [OPTIONS] COMMAND [ARGS]...
  "python3 CLIMain.py COMMAND --help" for more details
  
Options:
  --help  Show this message and exit.

Commands:
  lmulti
  lnested
  parseboogie
  parsectoboogie
  parsectopy

As we can see, SVMRanker provides five commands. The first two commands allow for proving termination of a given program while the remaining three can be used for parsing the input file and translate it to a different format. In the remaining part of the section we focus on the details for the use of the lmulti and lnested commands.

lmulti, short for learning multiphase ranking function, instructs SVMRanker to learn a multiphase ranking function for the given program. To get the detailed usage information for this command, one can use the following command.