在本文中，我们研究程序验证中的中心问题，即循环不变量和秩函数的生成。首先，我们使用迁移系统来描述程序；然后，将多项式程序的循环不变量和秩函数的生成归结为解半代数系统；最后，根据我们关于半代数系统求解理论和工具得到给定形式的不变量和秩函数。根据我们的方法，生成的不变量可以表示为一个半代数系统，而以前的方法只能生成方程形式的不变量，因此我们生成的不变量表达能力更强。 以前寻找秩函数的方法只能找到线性程序的线性秩函数，但是我们的方法一方面可以应用到多项式程序，另一方面可以生成非线性秩函数。 此外，们还把不变量的生成算法扩展到混成系统不变量的生成上。混成系统的不变量对证明混成系统的安全性和可达性等性质有着重要的作用。同时，我们的方法是完备的，也就是说，如果给定的多项式程序存在半代数系统形式的不变量和多项式秩函数，我们的方法一定能够得到它们。使用计算机代数工具DIscOVERER和QEPcAD，我们演示如何将我们的方法应用到许多实际程序中去。