User Tools

Site Tools


main

Differences

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

Link to this comparison view

Next revision
Previous revision
main [2020/11/20 14:03] – 外部编辑 127.0.0.1main [2020/12/01 12:48] (current) – [SVMRanker] merlin
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:main.png?nolink|}}**[[main| Main ]]{{:svmranker:tool.png?nolink|}}[[tool| Tool ]]{{:svmranker:usage.png?nolink|}}[[usage| Usage & Case Study ]] **  
 ====== SVMRanker======  ====== SVMRanker====== 
 SVMRanker, an open source tool implementing a general framework for proving termination of programs, SVMRanker, an open source tool implementing a general framework for proving termination of programs,
 which can synthesize ranking functions for programs with which can synthesize ranking functions for programs with
 both linear and polynomial updates, using SVM techniques to 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+synthesize ranking functions. SVMRanker is built on top of the prototype used in [4] and it adds
 support for learning **multiphase ranking functions**. \\ 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]]. SVMRanker is now publicly available on GitHub at [[https://github.com/ESEC-FSE-2020-Tool-Demo-ID21/SVMRanker|this repository]].
Line 28: Line 28:
  
  
-===== 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 ===== ===== 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).   - 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.   - 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.   - 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.   - Michael Colón and Henny Sipma. 2001. Synthesis of Linear Ranking Functions. In TACAS (LNCS, Vol. 2031). 67–81.
main.1605852203.txt.gz · Last modified: 2020/11/20 14:03 (external edit)