Differences

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

--- svmranker:main [2020/11/17 21:25] – 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 & Case Study ]] **
-====== 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
-----
-====== Future Work ======
-  * Support more types of templates, such as fractional and with n-roots, and ranking functions, such as lexicographic ranking functions, piece-wise ranking functions and so on, as described in [1].
-  * Strengthen the ability of SVMRanker to prove nontermination, as currently only fixed-point checking is implemented.
-  * Synthesizing coefficients of ranking functions with deep neural networks.