| 命令式程序终止性验证方法综述 |
| |
| 引用本文： | 李仁见,王昭飞.命令式程序终止性验证方法综述[J].计算机工程与应用,2011,47(28):1-6. |
| |
| 作者姓名： | 李仁见 王昭飞 |
| |
| 作者单位： | 国防科技大学计算机学院并行与分布处理国家重点实验室,长沙,410073 |
| |
| 基金项目： | 国家自然科学基金(No.60725206); 国家973项目课题(No.2011CB302603)~~ |
| |
| 摘 要： | 作为软件完全正确性的重要组成部分,程序终止性受到越来越多的关注。旨在跟踪国内外针对命令式程序的终止性验证方法,调研该领域的最新研究成果,同时提出解决该问题的建议性方法框架,对命令式程序终止性研究提供有意义的帮助。给出了程序终止性问题的定义,介绍了已有的数值程序、堆操作程序终止性验证方法,并分别进行了分析与对比。总结了当前研究中存在的难点与热点问题,给出了一种基于模型检验的C程序终止性验证框架,该框架可以作为研究命令式程序终止性的基本框架。
|
| 关 键 词： | 终止性 命令式程序 秩函数 尺寸变化终止(SCT)分析 模型检验 |
| 修稿时间： | |
Overview of termination verification methods for imperative programs |
| |
| LI Reniian,WANG Zhaofei.Overview of termination verification methods for imperative programs[J].Computer Engineering and Applications,2011,47(28):1-6. |
| |
| Authors: | LI Reniian WANG Zhaofei |
| |
| Affiliation: | LI Renjian,WANG Zhaofei National Laboratory for Parallel and Distributed Processing,School of Computer Science,National University of Defense Technology,Changsha 410073,China |
| |
| Abstract: | As an important integral part of the full correctness of software,termination property of programs has gained more and more attention.This paper tries to investigate the termination verification methods for imperative programs both at home and abroad,and concludes the newest research results.A suggestion solution for this problem is also presented,which is helpful for future researches.The problem of program termination is defined.Existing termination verification methods for numeric programs and heap manip... |
| |
| Keywords: | termination imperative program ranking function Size-Change Termination(SCT)analysis model checking |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与应用》浏览原始摘要信息 |
|
点击此处可从《计算机工程与应用》下载全文 |
