svmranker:main
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
svmranker:main [2020/11/18 19:23] – [SVMRanker] ::1 | svmranker:main [Unknown date] (current) – removed - external edit (Unknown date) 127.0.0.1 | ||
---|---|---|---|
Line 1: | Line 1: | ||
- | | ||
- | ====== 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 [3] and it adds | ||
- | support for learning multiphase ranking functions | ||
- | ---- | ||
- | ===== 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 singlephase | ||
- | 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. | ||
- | ---- | ||
- | |||
- | |||
- | |||
- | ===== 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, | ||
- | |||
- | * 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. |