近年来，随着软件规模的越来越大，软件的安全越来越被人们所关注，而现有软件开发方法及软件测试手段所能提供的安全保证是脆弱和不可靠的。即使经过多次测试后的软件，也不能确保其正确性。如何保证程序的正确性、提高软件的可信度一直是计算机科学界高度关注的一个重要问题，也是推动计算机科学发展的主要动力之一。　　 程序验证是研究程序正确性的理论，主要涉及到程序的正确性验证和终止性验证。不包括终止性分析的验证被称为程序的部分正确性证明。因此，程序的终止性分析是保证程序完全正确性的必要基础。目前，国内外对终止性的研究主要从两个方面进行：一方面，采用代数理论严格分析并证明循环的终止性，这种方法可以给出程序终止性判定的完备算法；另一方面，利用Floyd，Hoare，Dijkstra等人提出的归纳断言方法去自动验证程序的终止性，主要涉及到Ranking函数的合成和不变量的发现。　　 近年来，随着计算机代数的不断发展，许多代数方法被引入到程序验证领域，如抽象解释、量词消去等技术，极大的推动了程序验证研究的发展，产生了许多有意义的结论。本文在前人的基础上，结合实代数理论和计算机代数工具，对自动程序验证领域中的终止性和不变量两个关键性问题进行了深入地研究，提出了新的代数算法。　　 本文的创新点在于：　　 ·在Ranking函数合成过程中，采用多项式完全判别系统理论对过程函数Q(ε){>，≥0}，消去全局量词(ε){>，≥0}，该方法没有使用QEPCAD。相较于QEPCAD的方法，该方法效率更高。　　 ·试探性的提出了Non-Ranking函数的概念，使得构造Non-Ranking函数成为验证程序不终止的一个充分条件，该方法可以和合成Ranking函数的方法并行进行，提高了终止性判定的效率：　　 ·利用不动点理论，利用不动点理论，对定义在多个区间上的非线性循环程序进行了终止性研究。研究表明，当添加区间端点值的符号限制以后，该类多区间非线性循环程序的终止性是可判定的，并给出了相应的判定算法和参系数的离线判定系统；　　 ·对一类赋值矩阵为(准)线性方程组的循环程序，证明了其终止性是可以判定的，并给出了相应的判定方法。