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

武斌，理学博士，副教授，上海财经大学浙江学院统计系副主任，主要从事算法设计、机器学习等方面的研究。2013年荣获“浙江省第三届师德先进个人”和“金华市师德楷模”荣誉称号；2015年入选金华市321专业技术人才第二层次；2017年入选浙江省“十三五”高等学校学科专业带头人培养对象。近五年来，参与完成国家及省部级课题4项，主持或参与完成厅级课题5项，发表EI检索论文8篇。

前言
第一章 绪论
1.1 程序正确性研究方法概述
1.2 程序正确性研究概况
1.3 符号计算简介
第二章 循环不变式的自动生成
2.1 参系数半代数系统的实解分类及应用
2.2 有限点集消去理想的Grobner基
2.3 基于消去理想的循环不变式自动生成
2.4 本章小结
第三章 一类非线性循环程序的终止性分析
3.1 齐次多项式函数循环条件的程序终止性分析
3.2 一般情形
3.3 本章小结
第四章 循环程序终止的前置条件的自动生成
4.1 差分方程组的求解
4.2 前置条件的自动生成算法
4.3 本章小结
第五章 结束语
参考文献
致谢