中文版 | English
CSpace
Synthesizing ranking functions for loop programs via SVM
Li, Yi1; Li, Xie2,3; Li, Yong2; Sun, Xuechao2,3; Turrini, Andrea2,4; Zhang, Lijun2,3,4,5
2022-10-31
摘要Termination of programs is probably the most famous undecidable problem in computer science. Despite this undecidability result, a lot of effort has been spent on improving algorithms that prove termination of loops, which is one of the fundamental aspects of software reliability analysis. These algorithms usually focus on finding an appropriate ranking function for the loop, which proves its termination. In this paper, we focus on handling the synthesis problem of nested ranking functions and multi-phase ranking functions for loop programs. We first reduce the problem of a nested ranking function synthesis to the existence problem of a hyperplane separating classes of data. This allows us to leverage Support-Vector Machines (SVM) techniques for the synthesis of nested ranking functions. SVM are supervised learning algorithms that are used to classify data; they work by finding a hyperplane separating data points parted into two classes. We show how to carefully define the data points so that the separating hyperplane gives rise to a nested ranking function for the loop. Then we use this algorithm for nested ranking functions synthesis as a subprocedure to devise a sound algorithm which incrementally synthesizes multi-phase ranking functions. Experimental results confirm the effectiveness of our SVM-based synthesis of nested and multi-phase ranking functions.(c) 2022 Published by Elsevier B.V.
关键词Program analysis Termination Nested ranking function Multi -phase ranking function Support vector machine
DOI10.1016/j.tcs.2022.07.002
发表期刊THEORETICAL COMPUTER SCIENCE
ISSN0304-3975
卷号935页码:1-20
通讯作者Li, Yong(liyong@ios.ac.cn) ; Zhang, Lijun(zhanglj@ios.ac.cn)
收录类别SCI
WOS记录号WOS:000869995700001
语种英语