Differences

This shows you the differences between two versions of the page.

--- svmranker:main [2020/11/17 21:01] – merlin
+++ svmranker:main [Unknown date] (current) – removed - external edit (Unknown date) 127.0.0.1
@@ Line 1: / Line 1: @@
- **[[svmranker:main| Main ]]** || **[[svmranker:main| Tool ]]** ||  **[[svmranker:usage| Usage ]] **
-====== Introduction ======
-SVMRanker is a general framework for proving termination of loop programs.SVMRanker utilizes SVM techniques to synthesize multiphase ranking functions to prove program termination.
-----
-====== Installation ======
-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.
-===== Install Python packages =====
-  pip3 install z3-prover
-  pip3 install click
-  pip3 install sklearn
-  pip3 install python-constraint
-----
-====== Usage ======
-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.