SVMRanker is a general framework for proving termination of loop programs.SVMRanker utilizes SVM techniques to synthesize multiphase ranking functions to prove program termination.

• 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.

1. Jan Leike and Matthias Heizmann. 2015. Ranking Templates for Linear Loops. LMCS 11, 1 (2015).
2. 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.
3. 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.
4. Michael Colón and Henny Sipma. 2001. Synthesis of Linear Ranking Functions. In TACAS (LNCS, Vol. 2031). 67–81.