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

摘要：

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

关键词：程序验证、易变数据结构、结构归纳、自动定理证明

分类号：TP312(计算技术、计算机技术)

在线出版日期：2017-08-16（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：61-66,58