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

QQ客服 官方微博 反馈留言

	基于迭代轨迹划分的单分支循环程序终止性分析
	王垚; 李轶
	2023
摘要	秩函数作为循环程序终止性分析的重要方法已得到广泛研究。文中着重研究了单分支循环的终止性。首先提出了双向迭代循环概念,将单分支循环分为双向迭代循环和非双向迭代循环。其次,针对双向迭代循环程序,建立了一种划分思路,提出了三段式秩函数的概念,并证明了若该双向迭代循环存在三段式秩函数,则其是终止的。而对非双向迭代循环,引用增函数的划分思路,即利用增函数将原程序空间划分为更小的空间,并通过计算更小空间上的秩函数来证明原程序的终止性。最后,将三段式秩函数的计算问题归结为SVM分类问题,并利用工具Z3或bottema对由SVM所得的候选秩函数进行验证。
关键词	Program verification Ranking functions Machine learning Program termination 程序验证 秩函数 机器学习 程序终止性
发表期刊	计算机科学
ISSN	1002-137X
卷号	50期号:9页码:108-116
语种	中文