Trustworthy Intelligent Systems

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 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 single-phase 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.

Using SVMRanker

SVMRanker can be obtained from this page and used according to its usage instructions.

Main references

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