基于迭代轨迹划分的单分支循环程序终止性分析

摘要：

秩函数作为循环程序终止性分析的重要方法已得到广泛研究.文中着重研究了单分支循环的终止性.首先提出了双向迭代循环概念,将单分支循环分为双向迭代循环和非双向迭代循环.其次,针对双向迭代循环程序,建立了一种划分思路,提出了三段式秩函数的概念,并证明了若该双向迭代循环存在三段式秩函数,则其是终止的.而对非双向迭代循环,引用增函数的划分思路,即利用增函数将原程序空间划分为更小的空间,并通过计算更小空间上的秩函数来证明原程序的终止性.最后,将三段式秩函数的计算问题归结为SVM分类问题,并利用工具Z3或bottema对由SVM所得的候选秩函数进行验证.

关键词：程序验证、秩函数、机器学习、程序终止性

所属期刊栏目：50

分类号：TP311(计算技术、计算机技术)

在线出版日期：2023-09-20（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：108-116