计算最终线性秩函数的新方法

• 作者: 吴文渊 朱广 李轶
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 线性循环程序 终止性分析 最终线性秩函数 Mathematica
• 年，卷（期）: 2017,（1）
• 所属期刊栏目: 软件与数据库技术
• 页码范围: 194-198,213
• 页数: 6页
• 分类号: TP311.5
• 字数: 6733字
• 语种: 中文
• DOI: 10.11896/j.issn.1002-137X.2017.01.037

摘要

程序的终止性分析作为程序验证中重要的一环,在软件正确性验证中极为重要.对于一个线性循环程序,若该程序没有传统定义的线性秩函数,则基于传统定义的秩函数终止性分析方法失效.2013年,Bagnara提出了最终线性秩函数(Eventual Linear Ranking Functions)的定义,并证明了若某个程序存在最终线性秩函数,则该程序终止.由此,提出了新的方法来计算最终线性秩函数,构造了存在线性增函数和最终线性秩函数的等价半代数系统,并使用Mathematica工具对半代数系统进行求解,对比分析了各种最终秩函数求解方法的实际计算时间,结果证实了所提方法的优越性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李轶	中国科学院重庆绿色智能技术研究院	13	20	2.0	4.0
2	吴文渊	中国科学院重庆绿色智能技术研究院	19	79	6.0	8.0
3	朱广	中国科学院重庆绿色智能技术研究院	1	0	0.0	0.0