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

摘要：

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

关键词：线性循环程序、终止性分析、最终线性秩函数、Mathematica

所属期刊栏目：44

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金61572024,11471307;重庆市基础与前沿研究计划院士专项cstc2015jcyjys40001

在线出版日期：2017-04-10（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：194-198,213