基于迭代轨迹划分的单分支循环程序终止性分析
秩函数作为循环程序终止性分析的重要方法已得到广泛研究.文中着重研究了单分支循环的终止性.首先提出了双向迭代循环概念,将单分支循环分为双向迭代循环和非双向迭代循环.其次,针对双向迭代循环程序,建立了一种划分思路,提出了三段式秩函数的概念,并证明了若该双向迭代循环存在三段式秩函数,则其是终止的.而对非双向迭代循环,引用增函数的划分思路,即利用增函数将原程序空间划分为更小的空间,并通过计算更小空间上的秩函数来证明原程序的终止性.最后,将三段式秩函数的计算问题归结为SVM分类问题,并利用工具Z3或bottema对由SVM所得的候选秩函数进行验证.
程序验证、秩函数、机器学习、程序终止性
50
TP311(计算技术、计算机技术)
2023-09-20(万方平台首次上网日期,不代表论文的发表时间)
共9页
108-116