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/17 19:15] – [Usage] merlin | svmranker:main [2020/11/18 19:27] – [SVMRanker] ::1 | ||
---|---|---|---|
Line 1: | Line 1: | ||
- | [[:start| Main ]] || | + | **[[svmranker:main| Main ]]** || **[[svmranker: |
- | ====== | + | ====== |
- | SVMRanker | + | SVMRanker, an open source tool implementing |
+ | which can synthesize ranking functions for programs with | ||
+ | both linear and polynomial updates, using SVM techniques to | ||
+ | synthesize | ||
+ | support for learning **multiphase ranking functions**. | ||
+ | SVMRanker is now publicly available on GitHub at [[https:// | ||
---- | ---- | ||
- | ====== Installation ====== | + | ===== Background |
- | + | Deciding termination of programs is probably the most famous problem in computer science. | |
- | You should have installed Python 3 and Java Development Kit on your system. Currently we can successfully run SVMRanker with Python 3.7 and JDK 8.0. | + | And proving termination of loop programs is at the core of the termination analysis techniques used in Ultimate Automizer. |
- | ===== Install Python packages ===== | + | Now, synthesizing **ranking functions** for programs is a standard way to prove termination of loop programs:they map each program |
- | pip3 install z3-prover | + | 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. |
- | pip3 install click | + | |
- | pip3 install sklearn | + | |
- | pip3 install python-constraint | + | |
+ | **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. | ||
---- | ---- | ||
- | ====== Usage ====== | ||
- | In the following, we assume that current directory is SVMRanker. | ||
- | After having installed the required software, SVMRanker can be used by entering the src/ directory and then calling SVMRanker as follows: | + | |
- | python3 ./ | + | ===== Future Work ===== |
- | You should be able to see the following output. | + | |
- | | + | |
- | Usage: CLIMain.py [OPTIONS] COMMAND [ARGS]... | + | |
- | " | + | |
- | + | ||
- | Options: | + | |
- | --help | + | |
| | ||
- | | + | |
- | lmulti | + | |
- | lnested | + | |
- | parseboogie | + | |
- | parsectoboogie | + | |
- | parsectopy | + | |
- | As we can see, SVMRanker provides five commands. The first two commands allow for proving termination of a given program while the remaining three can be used for parsing the input file and translate it to a different format. In the remaining part of the section we focus on the details for the use of the lmulti and lnested commands. | + | |
- | + | ||
- | lmulti, short for learning multiphase ranking function, instructs | + | |
+ | * 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. |