Differences

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

--- svmranker:main [2020/11/17 21:33] – merlin
+++ svmranker:main [2020/11/20 14:03] – merlin
@@ Line 1: / Line 1: @@
- **[[svmranker:main| Main ]]** ||  **[[svmranker:main| Tool ]]** ||  **[[svmranker:usage| Usage & Case Study ]] **
+{{: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 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]].
 ----
+===== 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 =====