中文摘要：

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

英文摘要：

As an important integral part of the full correctness of software, termination property ot programs has gameo 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.