循环程序的界函数合成

谭旺; 李轶

首页> 中文期刊> 《计算机应用》 >循环程序的界函数合成

循环程序的界函数合成

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

作为循环程序终止性分析的主流方法,当前的秩函数方法大多局限于线性或多项式秩函数的求解。针对循环程序若不存在对应的线性或多项式秩函数,现有秩函数方法就无法证明其终止性的问题,提出一个新的方法来合成给定循环程序对应的界函数。对于给定的循环程序,倘若能找到其界函数,则表明该循环程序是可终止的。首先将界函数的求解问题转化为一个线性二分类问题,并在选定界函数模板后,根据模板建立映射关系以构建训练集;然后利用所得训练集通过支持向量机(SVM)获取分类超平面进而求解得到模板系数,从而得到候选的界函数;最后利用现有的符号验证工具Redlog对该候选界函数进行验证。实验结果表明,相较于现有的秩函数方法,所提方法不仅能够应用于更多的循环程序,而且所得界函数在形式上相较于秩函数更加简化。具体表现为,对于某些没有线性秩函数的循环,该方法可以得到其对应的线性界函数;同时,对于某些只有多阶段线性秩函数的循环,该方法可以求解得到全局的线性界函数。

著录项

来源
《计算机应用》 |2022年第2期|565-573|共9页
作者
谭旺; 李轶;
展开▼
作者单位

中国科学院重庆绿色智能技术研究院;

中国科学院大学计算机科学与技术学院;

展开▼
原文格式 PDF
正文语种 chi
中图分类程序设计、软件工程;
关键词
程序验证; 循环程序终止性; 支持向量机; 界函数; 秩函数;

相似文献

中文文献
外文文献
专利

1. 试论循环不变式和囿界函数在循环研制中的地位和作用 [J] . 游晓明 ,刘升 . 湖北师范学院学报：自然科学版 . 1998,第006期
2. 关于有界变差函数的复合函数仍为有界变差函数的条件 [J] . 古定桂 . 嘉应大学学报 . 1994,第002期
3. 序列偶循环相关函数及其界的研究 [J] . 常迎辉 ,许成谦 ,梁清梅 . 无线电通信技术 . 2006,第001期
4. 循环界函数的应用及求取方法 [J] . 王彩芬 . 西北师范大学学报：自然科学版 . 1996,第003期
5. 有界闭区间并上的非线性循环程序的终止性验证 [J] . 李玲娜 ,田继东 ,刘德斌 . 计算机应用与软件 . 2012,第010期
6. 有界闭区间并上的非线性循环程序的终止性验证 [C] . Li Ling-Na ,李玲娜 ,Tian Ji-Dong . 2012中国计算机大会 . 2012
7. 有界变差函数和ω-型有界变差函数的逼近 [A] . 叶秀芳 . 2004

循环程序的界函数合成

摘要

著录项

相似文献

相关主题

期刊订阅