svmranker:main
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revisionNext revisionBoth sides next revision | ||
svmranker:main [2020/11/18 19:25] – [Background] ::1 | svmranker:main [2020/11/18 19:36] – [SVMRanker] merlin | ||
---|---|---|---|
Line 5: | Line 5: | ||
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 [3] and it adds | ||
- | support for learning multiphase ranking functions | + | support for learning |
+ | SVMRanker is now publicly available on GitHub at [[https:// | ||
---- | ---- | ||
===== Background ===== | ===== 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. | ||
- | Now, synthesizing ranking functions for programs is a standard way to prove termination of loop programs:they map each program | + | Now, synthesizing |
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. | 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** | + | **Multiphase ranking |
for each phase; each phase covers a part of the whole state space | 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 | of the program and inside such subspace, the function is a singlephase |