程序验证是计算机程序设计领域的前沿研究课题,如何保证程序正确性是计算机科学的一个重大挑战.近年来,随着符号计算理论的不断完善和程序验证中使用精确无误差的数学方法的要求,使用符号计算理论来解决程序验证中的相关问题被认为是一种有效途径.本文利用符号计算的思想和方法研究了程序验证领域的三个基本问题：循环不变式生成、程序终止性分析以及前置条件生成.循环不变式在程序的部分正确性验证中起着非常重要的作用,如何生成循环不变式也是程序验证领域的挑战之一.本文主要研究了多项式循环程序的不变式生成问题.首次将有限点集消去理想的思想和方法应用于多项式循环程序的不变式生成,设计了一个多项式时间复杂度的循环不变式自动生成算法,可生成多项式等式型循环不变式.程序的终止性分析问题也是长期以来为众多计算机科学家所关注的问题之一.本文主要研究了一类带有非线性循环条件和线性赋值的循环程序的终止性分析问题.通过计算线性赋值矩阵的约当标准型,确定循环条件在循环次数充分大时的符号,将这类循环程序的终止性分析问题转化为判断参系数半代数系统有无实解的问题.如果参系数半代数系统中的左端函数个数有限或者左端函数都具有整数周期,则这类非线性循环程序的终止性问题是可判定的.另外一个值得研究的问题是如何计算合理的前置条件,使得循环程序在满足该条件的前提下是终止的.本文基于一阶常系数差分方程组的求解技术,设计了一个高效、实用的前置条件生成算法.我们将程序的循环赋值语句转化为程序变量关于循环次数的差分方程组,计算差分方程组的闭形式解.然后将闭形式解代入循环条件,在循环次数充分大时,判断循环条件的符号,进而生成循环程序合理的前置条件.针对线性赋值程序给出了一个高效、实用的前置条件自动生成算法.进而,对于可求出闭形式解的非线性赋值循环程序以及运算可交换的多分支循环程序,也做了相应研究.研究结果表明,符号计算是验证程序正确性的一种行之有效的方法.我们期待将符号计算中的一些经典算法更深入、广泛地应用到程序验证,并集成、研发新的有前途的验证工具.