基于Z3的Coq自动证明策略的设计和实现

来源：软件学报杂志2017年第4期北京时间：

作者：张恒若,付明

单位：张恒若，中国科学技术大学 信息科学技术学院, 安徽 合肥 23002611,付明，中国科学技术大学 计算机科学与技术学院, 安徽 合肥 230026;中国科学技术大学 苏州研究院软件安全实验室, 江苏 苏州 21512302

摘要：形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性，这种验证方式表达力强，可以证明复杂系统，但是自动化程度低、验证代价比较高；而使用程序验证器接受经过规范标注的源代码生成验证条件，并将验证条件交给约束求解器自动求解，这种方式自动化程度高，缺点在于它很难验证复杂系统软件的全部功能的正确性.结合上述两种方式的优点，在定理证明工具Coq中实现了一个自动证明策略smt4coq，它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题，提高了自动化验证的程度，减少了用户手动验证程序的开销.

关键词：形式化验证;定理证明工具;约束求解器;Coq;Z3

基金资助：国家自然科学基金（61103023，61229201，61379039，91318301，61632005）