| 一类带初始输入的线性循环终止性分析 |
| |
| 引用本文： | 李轶,李传璨,吴文渊.一类带初始输入的线性循环终止性分析[J].四川大学学报(工程科学版),2014,46(5):81-87. |
| |
| 作者姓名： | 李轶 李传璨 吴文渊 |
| |
| 作者单位： | 重庆邮电大学，计算机科学与技术学院,中国科学院重庆绿色智能技术研究院，自动推理与认知重庆市重点实验室,中国科学院重庆绿色智能技术研究院，自动推理与认知重庆市重点实验室 |
| |
| 基金项目： | 1.国家自然科学基金“几类while循环终止性分析的理论、方法及其应用”（No.61103110）；2.重庆市科技攻关重点项目“软件正确性分析的自动推理方法及工具的开发”（cstc2012ggB40004） |
| |
| 摘 要： | 本文针对带初始输入的二维齐次线性循环的终止性问题进行研究。通过分析该类循环所有非终止点组成集合(即NT集)的性质，将该类循环NT集的构造问题转化为一类非线性优化求解问题，并给出了此类优化问题的数学模型。最终，通过验证该类循环的初始输入是否位于所构造的NT集合内，判定了带初始输入的二维齐次线性循环的终止性, 并建立了用来完备判定该类循环终止性的算法。
|
| 关 键 词： | 可信软件 循环终止性 最优化问题 QEPCAD |
| 收稿时间： | 2014/2/24 0:00:00 |
| 修稿时间： | 7/4/2014 12:00:00 AM |
Termination Analysis of a Class of Initialized Linear Loops |
| |
| Li Yi,Li Chuancan and Wu Wenyuan.Termination Analysis of a Class of Initialized Linear Loops[J].Journal of Sichuan University (Engineering Science Edition),2014,46(5):81-87. |
| |
| Authors: | Li Yi Li Chuancan and Wu Wenyuan |
| |
| Affiliation: | Chongqing Key Laboratory of Automated Reasoning and Cognition CIGIT, CAS, |
| |
| Abstract: | This paper studies the termination of the initialized two variable homogeneous linear loops. By analyzing the property of the set NT composed of all nonterminating points, the problem about the construction of NT is converted to a class of nonlinear optimization problem. More importantly, by verifying whether or not the initial input of such loops lies in set NT, we can check the termination of the initialized two variable homogeneous linear loops completely. |
| |
| Keywords: | trustworthy software loop termination optimization problem QEPCAD |
|
| 点击此处可从《四川大学学报(工程科学版)》浏览原始摘要信息 |
|
点击此处可从《四川大学学报(工程科学版)》下载全文 |
