程序验证是计算机程序设计领域的前沿研究课题，如何保证程序正确性是计算机科学的一个重大挑战。近年来，随着符号计算理论的不断完善和程序验证中使用精确无误差的数学方法的要求，使用符号计算理论来解决程序验证中的相关问题被认为是一种有效途径。 《程序正确性证明方法》在前人研究的基础上，利用符号计算的思想和方法研究了程序验证领域的三个基本问题：循环不变式生成、程序终止性分析以及前置条件生成。
