Differences

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

--- svmranker:main [2020/11/17 21:02] – merlin
+++ svmranker:main [2020/11/20 14:03] – merlin
@@ Line 1: / Line 1: @@
- **[[svmranker:main| Main ]]** || **[[svmranker:main| Tool ]]** ||  **[[svmranker:usage| Usage ]] **
+{{:svmranker:main.png?nolink|}}**[[svmranker:main| Main ]]{{:svmranker:tool.png?nolink|}}[[svmranker:tool| Tool ]]{{:svmranker:usage.png?nolink|}}[[svmranker:usage| Usage & Case Study ]] **
-====== Introduction ======
+====== SVMRanker======
-SVMRanker is a general framework for proving termination of loop programs.SVMRanker utilizes SVM techniques to synthesize multiphase ranking functions to prove program termination.
+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 [3] and it adds
+support for learning **multiphase ranking functions**. \\
+SVMRanker is now publicly available on GitHub at [[https://github.com/ESEC-FSE-2020-Tool-Demo-ID21/SVMRanker|this repository]].
 ----
-====== Installation ======
+===== Background =====
+Deciding termination of programs is probably the most famous problem in computer science.
-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.
+And proving termination of loop programs is at the core of the termination analysis techniques used in Ultimate Automizer.
-===== Install Python packages =====
+Now, synthesizing **ranking functions** for programs is a standard way to prove termination of loop programs：they map each program
-  pip3 install z3-prover
+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.
-  pip3 install click
-  pip3 install sklearn
-  pip3 install python-constraint
+**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.
 ----
+===== 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.
+----
+===== Main References =====
+  - Jan Leike and Matthias Heizmann. 2015. Ranking Templates for Linear Loops. LMCS 11, 1 (2015).
+  - Ben-Amram A.M., Genaim S. (2017) On Multiphase-Linear Ranking Functions. In: Majumdar R., Kunčak V. (eds) Computer Aided Verification. CAV 2017. Lecture Notes in Computer Science, vol 10427. Springer, Cham.
+  - Yi Li, Xuechao Sun, Yong Li, Andrea Turrini, and Lijun Zhang. 2019. Synthesizing Nested Ranking Functions for Loop Programs via SVM. In ICFEM (LNCS, Vol. 11852). 438–454.
+  - Michael Colón and Henny Sipma. 2001. Synthesis of Linear Ranking Functions. In TACAS (LNCS, Vol. 2031). 67–81.