中国科学院重庆绿色智能技术研究院机构知识库

QQ客服 官方微博 反馈留言

	Synthesizing Nested Ranking Functions for Loop Programs via SVM
	Li, Yi1; Sun, Xuechao2,3; Li, Yong2,3; Turrini, Andrea2,4; Zhang, Lijun2,3,4
	2019
摘要	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 building blocks of software reliability analysis. These algorithms are usually focused on finding an appropriate ranking function for the loop, which proves its termination. In this paper, we consider nested ranking functions for loop programs and show that the existence problem of a nested ranking function is equivalent 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. Experimental results confirm the effectiveness of our SVM-based synthesis of nested ranking functions. © 2019, Springer Nature Switzerland AG.
语种	英语
DOI	10.1007/978-3-030-32409-4_27
会议(录)名称	21st International Conference on Formal Engineering Methods, ICFEM 2019
页码	438-454
收录类别	EI
会议地点	Shenzhen, China
会议日期	November 5, 2019 - November 9, 2019