| 断言语言支持自定义谓词的程序验证器原型 |
| |
| 引用本文： | 徐文义,陈意云,李兆鹏. 断言语言支持自定义谓词的程序验证器原型[J]. 小型微型计算机系统, 2013, 34(7) |
| |
| 作者姓名： | 徐文义 陈意云 李兆鹏 |
| |
| 作者单位： | 中国科学技术大学计算机科学与技术学院,合肥230026;中国科学技术大学苏州研究院软件安全实验室,江苏苏州215123 |
| |
| 摘 要： | 基于逻辑推理的方法进行程序验证是形式化程序验证的研究热点.目前的自动验证工具为了保证自动性,对描述程序性质的断言语言都有较多限制,导致程序的某些递归性质难以用断言语言表述.本文在一个面向指针程序、基于先前自行设计的形状图逻辑、依赖于自动定理证明工具Z3的自动程序验证原型系统上,通过在断言语言中引入自定义谓词来增强断言语言的表达能力,使得该原型系统不仅能自动验证含操作易变数据结构的程序的性质,也能自动验证一些不含指针的程序的性质.
|
| 关 键 词： | 程序验证 Hoare逻辑 形状图逻辑 程序分析 自定义谓词 |
Verifier Prototype for Programs with User-defined Predicates in the Assertion Language |
| |
| XU Wen-yi , CHEN Yi-yun , LI Zhao-peng. Verifier Prototype for Programs with User-defined Predicates in the Assertion Language[J]. Mini-micro Systems, 2013, 34(7) |
| |
| Authors: | XU Wen-yi CHEN Yi-yun LI Zhao-peng |
| |
| Abstract: | |
| |
| Keywords: | software safety hoare logic user-defined predicates verification prover |
| 本文献已被 万方数据 等数据库收录！ |
|
