计算机工程与应用2011，Vol.47Issue(28)：1-6,105,7.DOI:10.3778/j.issn.1002-8331.2011.28.001
命令式程序终止性验证方法综述
Overview of termination verification methods for imperative programs
摘要
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 manipulating programs are introduced and compared separately.The hard problems and hot topics are also concluded and presented.A termination verification framework for C programs is presented and that can work as a starting framework for researching the termination property of imperative programs.关键词
终止性/命令式程序/秩函数/尺寸变化终止(SCT)分析/模型检验Key words
termination/imperative program/ranking function/Size-Change Termination(SCT) analysis/model checking分类
信息技术与安全科学引用本文复制引用
李仁见,王昭飞..命令式程序终止性验证方法综述[J].计算机工程与应用,2011,47(28):1-6,105,7.基金项目
国家自然科学基金(the National Natural Science Foundation of China under Grant No.60725206) （the National Natural Science Foundation of China under Grant No.60725206）
国家973项目课题(No.2011CB302603). （No.2011CB302603）
