易变数据结构归纳引理的自动证明

• 作者: 李薛剑 杨晨 罗奇鸣 陈意云
• 来源期刊: 电子技术
• 学科: 工学
• 关键词: 程序验证 易变数据结构 结构归纳 自动定理证明
• 年，卷（期）: 2017,（6）
• 所属期刊栏目: 电子技术设计与应用
• 页码范围: 61-66,58
• 页数: 7页
• 分类号: TP312
• 字数: 6293字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-0755.2017.06.020

摘要

程序性质的自动验证有时需要验证者提供相关的归纳引理,程序验证的结果可靠与否依赖于验证者所提供的归纳引理正确与否.本文围绕操作易变数据的程序的自动验证,设计并实现一个相关引理的自动证明器,作为程序自动验证器中检查验证者所提供的归纳引理是否正确的工具.该证明器分析所有待证归纳引理,构建引理之间的依赖关系图,得出引理的证明顺序.对每个引理,分析得出它的归纳变元和应采用的归纳方法,把归纳证明的各步交给自动定理证明器Z3进行证明.该证明器的原型已嵌入一个基于演绎推理的安全C语言自动验证系统中,并成功验证了有序链表、二叉搜索树、AVL树、伸展树等数据结构的性质.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈意云	中国科学技术大学计算机科学与技术学院	83	854	16.0	26.0