Differences

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

--- svmranker:main [2020/11/17 21:34] – merlin
+++ svmranker:main [Unknown date] (current) – removed - external edit (Unknown date) 127.0.0.1
@@ Line 1: / Line 1: @@
- **[[svmranker:main| Main ]]** ||  **[[svmranker:tool| Tool ]]** ||  **[[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.
-----
-----
-===== 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.