|
|||||
|
|
| 一个用于指针程序验证的自动定理证明器的设计与实现 | |
| 作者姓名： | 王振明 陈意云 王志芳 |
| 作者单位： | (中国科学技术大学 计算机科学技术系,安徽 合肥 230026),(中国科学技术大学 苏州研究院 软件安全实验室,江苏 苏州 215123) |
| 基金项目： | 国家自然科学基金,Intel中国研究中心资助项目 |
| 摘 要： | 对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明. |
| 关 键 词： | 指针逻辑 验证条件 自动定理证明器 证明检查算法 |
| 修稿时间： | 1900-01-01 |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |
| 点击此处可从《小型微型计算机系统》浏览原始摘要信息 | |
| 点击此处可从《小型微型计算机系统》下载免费的PDF全文 | |