| 基于Z3的Coq自动证明策略的设计和实现 |
| |
| 引用本文： | 张恒若,付明.基于Z3的Coq自动证明策略的设计和实现[J].软件学报,2017,28(4):819-826. |
| |
| 作者姓名： | 张恒若 付明 |
| |
| 作者单位： | 中国科学技术大学 信息科学技术学院, 安徽 合肥 230026,中国科学技术大学 计算机科学与技术学院, 安徽 合肥 230026;中国科学技术大学 苏州研究院 软件安全实验室, 江苏 苏州 215123 |
| |
| 基金项目： | 国家自然科学基金（61103023，61229201，61379039，91318301，61632005） |
| |
| 摘 要： | 形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性，这种验证方式表达力强，可以证明复杂系统，但是自动化程度低、验证代价比较高，而使用程序验证器接受经过规范标注的源代码生成验证条件，并将验证条件交给约束求解器自动求解，这种方式自动化程度高，缺点在于它很难验证复杂系统软件的全部功能的正确性.本文结合上述两种方式的优点，在定理证明工具Coq中实现了一个自动证明策略smt4coq，它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题，提高了自动化验证的程度，减轻用户手动验证程序的开销.
|
| 关 键 词： | 形式化验证 定理证明工具 约束求解器 Coq Z3 |
| 收稿时间： | 2016/6/20 0:00:00 |
| 修稿时间： | 2016/9/8 0:00:00 |
Design and Implementation of Coq Tactics Based on Z3 |
| |
| ZHANG Heng-Ruo and FU Ming.Design and Implementation of Coq Tactics Based on Z3[J].Journal of Software,2017,28(4):819-826. |
| |
| Authors: | ZHANG Heng-Ruo and FU Ming |
| |
| Affiliation: | School of Information Science and Technology, University of Science and Technology of China, Hefei 230026 and School of Computer Science, University of Science and Technology of China, Hefei 230026;Software Security Lab., Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou 215123 |
| |
| Abstract: | |
| |
| Keywords: | formal verification proof assistant tools SMT solvers Coq Z3 |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
