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