| 汇编级顺序语句块的自动形式化规约及其验证 |
| |
| 引用本文： | 祁龙云,吕小亮,路红,黄皓. 汇编级顺序语句块的自动形式化规约及其验证[J]. 计算机工程, 2019, 45(10) |
| |
| 作者姓名： | 祁龙云 吕小亮 路红 黄皓 |
| |
| 作者单位： | 南京南瑞信息通信科技有限公司,南京,210003;南京大学计算机软件新技术国家重点实验室,南京,210023 |
| |
| 基金项目： | 国家电网公司总部科技项目 |
| |
| 摘 要： | 软件的形式化验证是保障软件可证明性、可靠性和安全性的重要手段,但传统形式化验证脚本的生成过程复杂且需要形式化验证专家的大量手工验证。为提高证明效率,构建一种自动证明模型,并在此基础上提出语义自动规约算法以及对所规约的语义自动生成证明脚本的算法。利用C++和Python并通过交互式定理证明器Isabelle 2017在基准数据中随机选择10个程序进行测试,结果表明,与完全人工操作相比,该算法具有较高的验证效率,可实现顺序语句块的自动化规约与验证。
|
| 关 键 词： | 自动形式化规约 自动化验证 定理证明器 交互式定理 形式化验证 |
Automatic Formal Specification and Its Verification of Assembly-Level Sequential Statement Blocks |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
