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

【Abstract】 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.更多还原