SVMRanker

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
{{:svmranker:main.png?nolink|}}**[[main| Main ]]{{:svmranker:tool.png?nolink|}}[[tool| Tool ]]{{:svmranker:usage.png?nolink|}}[[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 [4] 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.
----




===== Main References =====
  - Xie Li, Yi Li, Yong Li, Xuechao Sun, Andrea Turrini, and Lijun Zhang. 2020. SVMRanker: a general termination analysis framework of loop programs via SVM. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2020).
  - 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.