多分支单变量循环程序的终止性分析

来源：软件学报杂志2015年第2期北京时间：

作者：李轶,李传璨,吴文渊

单位：李轶，自动推理与认知重庆市重点实验室中国科学院 重庆绿色智能技术研究院, 重庆 40112011,李传璨，自动推理与认知重庆市重点实验室中国科学院 重庆绿色智能技术研究院, 重庆 401120;重庆邮电大学 计算机科学与技术学院, 重庆 40006502,吴文渊，自动推理与认知重庆市重点实验室中国科学院 重庆绿色智能技术研究院, 重庆 40112003

摘要：对多分支单变量循环程序的终止性问题进行了研究.证明了在适定的条件下,该类循环程序不可终止性的充分必要条件是迭代映射在循环条件形成的区域中有不动点.特别地,当这类循环程序是多项式循环程序时,在给定条件下,其在实数域上的终止性问题是可判定的.

关键词：可信计算;多分支循环程序;终止性分析

基金资助：国家自然科学基金(61103110); 重庆市科技攻关项目(cstc2012ggB40004, cstc2013jjys0002)