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

Automatic Proving for Inductive Lemmas of Mutable Data Structure

作　　者：杨晨[1,2] 罗奇鸣[1,2] 李薛剑[1,2] 陈意云[1,2] 

机构地区：[1]中国科学技术大学计算机科学与技术学院,安徽合肥230026 [2]中国科大先进技术研究院中国科大-国创高可信软件工程中心,安徽合肥231283

出　　处：《电子技术（上海）》2017年第6期61-66,58,共7页Electronic Technology

摘　　要：程序性质的自动验证有时需要验证者提供相关的归纳引理,程序验证的结果可靠与否依赖于验证者所提供的归纳引理正确与否。本文围绕操作易变数据的程序的自动验证,设计并实现一个相关引理的自动证明器,作为程序自动验证器中检查验证者所提供的归纳引理是否正确的工具。该证明器分析所有待证归纳引理,构建引理之间的依赖关系图,得出引理的证明顺序。对每个引理,分析得出它的归纳变元和应采用的归纳方法,把归纳证明的各步交给自动定理证明器Z3进行证明。该证明器的原型已嵌入一个基于演绎推理的安全C语言自动验证系统中,并成功验证了有序链表、二叉搜索树、AVL树、伸展树等数据结构的性质。Automated verification of program properties may require related inductive lemmas from programmers, whose soundness affect the reliability of verification results. This paper has designed and implemented an automated tool for proving such lemmas in the context of verifying heap-manipulating data structures. First, it constructs a dependency relation graph among lemmas to obtain an order for proving them. Then, for each lemma it extracts the inductive variables, analyzes suitable proof strategies, and employs satisfiability modulo theories（SMT） solvers to prove each inductive step. A prototype of the proposed tool has been embedded into an automated verification system for the safe C language, which has successfully verified properties of data structures such as binary search trees, AVL trees, and splay trees, etc.

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

分 类 号：TP312[自动化与计算机技术—计算机软件与理论]