单分支线性约束循环程序的终止性分析
Termination Analysis of Single-path Linear Constraint Loops作者机构：中国科学院重庆绿色智能技术研究院自动推理与认知中心重庆400714 中国科学院大学北京100049
出 版 物：《软件学报》 (Journal of Software)
年 卷 期：2024年第35卷第3期
页 面：1307-1320页
核心收录：
学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）]
基 金：重庆市自然科学基金(cstc2019jcyj-msxmX0638) 国家自然科学基金(11771421) 中国科学院“西部之光”人才培养计划
摘 要：秩函数法是循环终止性分析的主要方法,秩函数的存在表明了循环程序是可终止的.针对单分支线性约束循环程序,提出一种方法对此类循环的终止性进行分析.基于增函数法向空间的计算,该方法将原程序空间上的秩函数计算问题归结为其子空间上的秩函数计算问题.实验结果表明,该方法能有效验证现有文献中大部分循环程序的终止性.
维普期刊数据库
同方期刊数据库