软件的顺序语句块自动化规约与验证研究

资料大小: 1.65 MB

所需积分: 0

下载次数:

用户评论: 0条评论,查看

上传日期: 2021-06-03

上 传 者: 他上传的所有资料

资料介绍

标签:C++(1078)自动化(2943)软件(2016)

  软件的形式化验证是保障软件可证明性、可靠性和安全性的重要手段,但传统形式化验证脚本的生成过程复杂且需要形式化验证专家的大量手工验证。为提高证明效率,构建一种自动证明模型,并在此基础上提出语义自动规约算法以及对所规约的语义自动生成证明脚本的算法。利用C++++和 Python并通过交互式定理证明器abelle2017在基准数据中随机选择10个程序进行测试,结果表明,与完全人工操作相比,该算法具有较高的验证效率,可实现顺序语句块的自动化规约与验证。

用户评论

查看全部 条评论

发表评论请先 , 还没有账号?免费注册

发表评论

用户评论
技术交流、我要发言! 发表评论可获取积分! 请遵守相关规定。
上传电子资料