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

摘要：

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

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

所属期刊栏目：47

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

资助基金：国家自然科学基金the National Natural Science Foundation of China under Grant 60725206;国家973项目课题2011CB302603

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

页数：共7页

页码：1-6,105