main
Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
| main [2020/11/23 16:48] – ::1 | main [2020/12/01 12:48] (current) – [SVMRanker] merlin | ||
|---|---|---|---|
| Line 4: | Line 4: | ||
| 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:// | SVMRanker is now publicly available on GitHub at [[https:// | ||
| ---- | ---- | ||
| - | ===== Background =====555 | + | ===== Background ===== |
| Deciding termination of programs is probably the most famous problem in computer science. | 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. | And proving termination of loop programs is at the core of the termination analysis techniques used in Ultimate Automizer. | ||
| 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, | ||
| - | * 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.1606121317.txt.gz · Last modified: 2020/11/23 16:48 (external edit)