Development of an automatic safety property prover with lemma discovery based on test

点击翻译按钮获取中文摘要

In this research, we developed an automatic invariant prover based on fixed-point induction with lemma discovery. To improve features of automatic verification and efficiencies, we implemented the weakest precondition computation with an SMT solver : CVC3, then implemented functions of fixed-point induction and lemma discovery with the computation. Using an SMT solver and lemma discovery, it could speed up more than ten times and prove a large scale problem.