Differences

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

--- svmranker:main [2020/11/20 14:03] – merlin
+++ svmranker:main [Unknown date] (current) – removed - external edit (Unknown date) 127.0.0.1
@@ Line 1: / Line 1: @@
-{{:svmranker:main.png?nolink|}}**[[svmranker:main| Main ]]{{:svmranker:tool.png?nolink|}}[[svmranker:tool| Tool ]]{{:svmranker:usage.png?nolink|}}[[svmranker:usage| Usage & Case Study ]] **
-====== SVMRanker======
-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]].
-----
-===== Background =====
-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.
-----
-===== 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.