资料下载
×
Z3的Coq自动证明策略的设计
消耗积分:1 |
格式:rar |
大小:1.03 MB |
2017-12-29
分享资料个
形式化验证方法被认为是一种构建高可信软件系统的有效手段．在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性，这种验证方式表达力强。可以证明复杂系统，但是自动化程度低、验证代价比较高；而使用程序验证器接受经过规范标注的源代码生成验证条件，并将验证条件交给约束求解器自动求解，这种方式自动化程度高，缺点在于它很难验证复杂系统软件的全部功能的正确性．结合上述两种方式的优点，在定理证明工具Coq中实现了一个自动证明策略smt4coq，它通过在Coq中调用约束求解器23自动证明32位机器整数相关的数学命题，提高了自动化验证的程度，减少了用户手动验证程序的开销．
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
评论(0)
发评论
- 相关下载
- 相关文章
