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

	计算最终线性秩函数的新方法
	朱广; 李轶; 吴文渊
刊名	计算机科学
	2017
卷号	044 期号:001 页码:194
ISSN号	1002-137X
英文摘要	程序的终止性分析作为程序验证中重要的一环，在软件正确性验证中极为重要。对于一个线性循环程序，若该程序没有传统定义的线性秩函数，则基于传统定义的秩函数终止性分析方法失效。2013年，Bagnara提出了最终线性秩函数（Eventual Linear Ranking Functions）的定义，并证明了若某个程序存在最终线性秩函数，则该程序终止。由此，提出了新的方法来计算最终线性秩函数，构造了存在线性增函数和最终线性秩函数的等价半代数系统，并使用Mathematica工具对半代数系统进行求解，对比分析了各种最终秩函数求解方法的实际计算时间，结果证实了所提方法的优越性。
语种	英语
内容类型	期刊论文
源URL	[http://119.78.100.138/handle/2HOD01W0/9233]
专题	中国科学院重庆绿色智能技术研究院
作者单位	中国科学院重庆绿色智能技术研究院
推荐引用方式 GB/T 7714	朱广,李轶,吴文渊. 计算最终线性秩函数的新方法[J]. 计算机科学,2017,044(001):194.
APA	朱广,李轶,&吴文渊.(2017).计算最终线性秩函数的新方法.计算机科学,044(001),194.
MLA	朱广,et al."计算最终线性秩函数的新方法".计算机科学 044.001(2017):194.