SVMRanker

User Tools

Site Tools

Trace:
svmranker:main

Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
Last revisionBoth sides next revision
svmranker:main [2020/11/18 19:18] – [SVMRanker] ::1svmranker:main [2020/11/20 14:03] – merlin
Line 1: Line 1:
- **[[svmranker:main| Main ]]** ||  **[[svmranker:tool| 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====== 
-SVMRanker v1.0 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 ===== ===== Background =====
 Deciding termination of programs is probably the most famous problem in computer science.  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. 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+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. 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+**Multiphase ranking functions** consist of multiple functions, one
 for each phase; each phase covers a part of the whole state space 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 of the program and inside such subspace, the function is a singlephase
Line 20: Line 25:
 the last phase, the loop program has been proved to be terminating. the last phase, the loop program has been proved to be terminating.
 ---- ----
 +
 +
  
 ===== Future Work ===== ===== Future Work =====