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

• 作者: 李仁见 王昭飞
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 终止性 命令式程序 秩函数 尺寸变化终止(SCT)分析 模型检验
• 年，卷（期）: 2011,（28）
• 所属期刊栏目: 博士论坛
• 页码范围: 1-6,105
• 分类号: TP311
• 字数: 11446字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.2011.28.001

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李仁见	国防科技大学计算机学院并行与分布处理国家重点实验室	3	4	2.0	2.0
2	王昭飞	国防科技大学计算机学院并行与分布处理国家重点实验室	3	2	1.0	1.0