命令式程序终止性验证方法综述

• 全文链接
• 请求原文

作   者：

李仁见;  王昭飞; 

作者机构：

国防科技大学计算机学院并行与分布处理国家重点实验室; 

关键词：

模型检验;  终止性;  命令式程序;  尺寸变化终止(SCT)分析;  秩函数; 

期刊名称：

计算机工程与应用

基金项目：

i s s n：

1002-8331

年卷期：

2011 年 47 卷 28 期

页   码：

1-6+105

摘   要：

作为软件完全正确性的重要组成部分,程序终止性受到越来越多的关注。旨在跟踪国内外针对命令式程序的终止性验证方法,调研该领域的最新研究成果,同时提出解决该问题的建议性方法框架,对命令式程序终止性研究提供有意义的帮助。给出了程序终止性问题的定义,介绍了已有的数值程序、堆操作程序终止性验证方法,并分别进行了分析与对比。总结了当前研究中存在的难点与热点问题,给出了一种基于模型检验的C程序终止性验证框架,该框架可以作为研究命令式程序终止性的基本框架。