本项目应用计算机代数和实代数中的深刻理论及成熟工具，采取符号与数值计算相结合的方法对广泛存在于实际应用中的几类线性和非线性循环程序的终止性进行分析和验证。. 我们主要从两个方面来进行循环程序的终止性分析。其一，从可判定的角度进行终止性分析。尽管程序终止性问题早在上世纪30年代就被Tiwari证明是不可判定的，但人们仍然热衷于去探寻可判定的子类。其二，采用合成Ranking函数的方式进行终止性分析。基于Ranking函数合成的验证方法并不是完备的。这是因为，虽然，Ranking函数的存在印证了循环程序是可终止的，但Ranking函数不存在却并不能说明循环程序是不可终止的。因此，Ranking函数的存在仅仅是循环程序可终止的充分而非必要的条件。尽管如此，基于Ranking函数的终止性验证方法仍是当今进行终止性分析的主流方法。. 首先，从可判定角度，我们对一类线性while循环程序的终止性问题进行了分析。这类循环在2004年首次被斯坦福教授Tiwari提出，并证明了它在实数域上的终止性是可判定的。但是，我们发现，在多数情形下，如果此类循环程序是不可终止的，那么，Tiwari的方法所给出的点是一个N-不可终止点，即这样的点需要再迭代N次后才能成为一个不可终止点。而在他的文章中也并没有给出N的计算方法。因此，基于这个发现，我们提出了一种方法去计算N的值。其次，基于赋值矩阵Jordan块的特殊结构，我们将这类线性循环程序的终止性问题归于为两类特殊线性程序的终止性问题。而后者的终止性更易被判定。更为重要的是，如果该类循环程序是不可终止的，那么，我们的新算法能构造至少一个不可终止点。本项目中，除了对上述的线性循环程序的终止性进行分析外，我们也研究了部分非线性循环程序的终止性。一般地，非线性循环程序的终止性因为其更为复杂的迭代动力行为，从而导致其终止性方面的研究甚少。通过分析无穷迭代序列在某些条件下所呈现出的良好性质，我们证明了三类非线性循环程序在实数域上的终止性是可判定的，并证明了其是不可终止的充要条件是迭代函数在循环条件所形成的区域中有不动点。. 其次，借助工具DISCOVERER和CDS理论，我们也建立了基于Ranking函数合成的终止性验证方法。新方法中，我们引进一些松弛变量，从而使得最终的半代数系统更容易让现有的工具去自动求解。