对程序进行分析和验证是当今计算机程序设计研究领域的前沿课题，如何保证程序按照人的预先设定严格执行而不出错是当今信息科学和可信计算技术与理论研究中的核心科学问题。近年来，随着符号计算理论的不断完善，利用精确的数学理论和方法对程序验证领域的相关问题进行研究的思路引起了越来越多的关注。　　 总的来说，程序验证领域包括三个侧重点各不同的研究方向：不变式生成、程序终止性验证以及程序可达性分析。三个方向在程序验证领域都有着各自的用途，具有不变式的程序是部分正确的；如果程序是部分正确的同时又是终止的，那么这个程序是完全正确的；如果程序中有语句不可到达，不能说程序是错误的，但应该警告有多余的或者没有起到预先设想的语句存在。相比较而言，不变式的存在和程序的可达性更加注重的是程序细节，而程序终止性验证更加注重的是程序的整体属性。总的来说，这三个方面辩证统一，对于程序验证缺一不可。但是三个方面的研究侧重又各有不同。因为程序终止性是保证程序正确的基础，所以本文主要在程序终止性的验证方面做了一定的研究。　　 在程序终止的前置条件生成方面，本文基于有限差分树相关概念和理论提出试差算子和相应的试差法，并设计了相应算法以生成线性循环程序终止的前置条件。当试差算子有限并且非零最高阶试差算子为负常数时，程序是终止的，此时前置条件即为任意初始值；当试差算子有限并且非零最高阶试差算子为正常数时，结合半代数系统及其工具Discoverer可以判断程序是否有不终止点；当试差算子有限并且非零最高阶试差算子为循环变量初值的表达式时，首先获得循环条件表达式为一多项式，再根据其主导项符号为负从而生成使程序终止的前置条件；当试差算子为一无限序列时，写出试差算子的通项公式，从而获得循环条件表达式的通项公式，再根据循环条件被破坏生成使其终止的前置条件。　　 由于利用试差算子不仅可以获得循环条件表达式的通项公式，也可以得到循环变量的通项公式，所以结合试差法和循环复杂度上界的计算，可以将循环程序终止转换为循环程序具有循环复杂度上界，从而验证程序是否终止。进一步地将这种方法用于部分含分支的线性循环程序的终止性验证上，因为含分支的线性循环程序可以转化为含嵌套循环的线性循环程序，那么含分支的线性循环程序终止当且仅当对应的含嵌套循环的线性循环程序具有确定的循环复杂度上界。本文试图利用这种技术验证角谷猜想的正确性，但随后发现由于内嵌循环的复杂度上界不能明确给出，以至于不能表示出外层循环的循环变量通项公式，无法验证外层循环具有循环复杂度上界，最终验证失败。虽然没有能验证成功，但这次实验却向我们揭露了一个事实，那就是最简单的含分支的线性循环程序其复杂度也是非常大的，所以在这个方面还需要更多理论的引入，并逐渐完备起来。　　 对于非线性循环程序而言，非线性系统固有的复杂性更是令人望而却步。本文首先利用试差法分析和验证了一些具有特殊函数形式的非线性循环程序的终止性。这应该视作是对非线性程序验证的一种有益尝试。此外，基于函数迭代与程序循环本质相同这一观点，借助吸引子的判断方法，本文还提出了一个实用的对区间上的非线性循环程序的终止性进行验证的算法，并得到一类特殊类型的循环程序在两个不相交区间并上不终止的验证方法。最后，基于符号动力学的相关理论，本文对在有限个不相交的有界区间上的非线性程序的终止性进行了分析，利用区间和函数的转换图，本文给出了具体的验证算法。