基于Z3的Coq自动证明策略的设计和实现
发布时间：2018-12-29 20:48
【摘要】：形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高;而使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.结合上述两种方式的优点,在定理证明工具Coq中实现了一个自动证明策略smt4coq,它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题,提高了自动化验证的程度,减少了用户手动验证程序的开销.
[Abstract]:Formal verification method is considered to be an effective method to construct high trusted software system. In theorem proving tool, the function correctness of the system software can be verified by manually writing the proof script. This verification method is expressive and can prove the complex system, but the automation degree is low, and the verification cost is high. The program validator is used to accept the standard annotated source code to generate the verification condition, and the verification condition is given to the constraint solver to solve it automatically. The drawback is that it is difficult to verify the correctness of all functions of complex system software. Combining the advantages of the above two methods, an automatic proof strategy, smt4coq, is implemented in the theorem proving tool Coq. By calling the constraint solver Z3 in Coq, we automatically prove the mathematical propositions related to 32-bit machine integers. It improves the degree of automatic verification and reduces the overhead of user manual verification program.
【作者单位】： 中国科学技术大学信息科学技术学院;中国科学技术大学计算机科学与技术学院;中国科学技术大学苏州研究院软件安全实验室;
【基金】：国家自然科学基金(61103023,61229201,61379039,91318301,61632005)~~
【分类号】：TP311.52
本文编号：2395377
[Abstract]:Formal verification method is considered to be an effective method to construct high trusted software system. In theorem proving tool, the function correctness of the system software can be verified by manually writing the proof script. This verification method is expressive and can prove the complex system, but the automation degree is low, and the verification cost is high. The program validator is used to accept the standard annotated source code to generate the verification condition, and the verification condition is given to the constraint solver to solve it automatically. The drawback is that it is difficult to verify the correctness of all functions of complex system software. Combining the advantages of the above two methods, an automatic proof strategy, smt4coq, is implemented in the theorem proving tool Coq. By calling the constraint solver Z3 in Coq, we automatically prove the mathematical propositions related to 32-bit machine integers. It improves the degree of automatic verification and reduces the overhead of user manual verification program.
【作者单位】： 中国科学技术大学信息科学技术学院;中国科学技术大学计算机科学与技术学院;中国科学技术大学苏州研究院软件安全实验室;
【基金】：国家自然科学基金(61103023,61229201,61379039,91318301,61632005)~~
【分类号】：TP311.52
【相似文献】
相关期刊论文 前1条
1 何锫;证明策略及其有效性问题[J];软件学报;1991年04期
相关硕士学位论文 前1条
1 曹景源;C程序证明策略在Coq中的设计和实现[D];中国科学技术大学;2015年
，本文编号：2395377
本文链接：https://www.wllwen.com/kejilunwen/ruanjiangongchenglunwen/2395377.html
