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

• Project/Area Number: 20800082
• Research Category: Grant-in-Aid for Young Scientists (Start-up)
• Allocation Type: Single-year Grants
• Research Field: Software
• Research Institution: National Institute of Advanced Industrial Science and Technology
• Principal Investigator: NAKANO Masahiro National Institute of Advanced Industrial Science and Technology, システム検証研究センター, 産総研特別研究員 (90470046)
• Project Period (FY): 2008 – 2009
• Project Status: Completed (Fiscal Year 2009)
• Budget Amount: ¥2,548,000 (Direct Cost: ¥1,960,000、Indirect Cost: ¥588,000); Fiscal Year 2009: ¥1,274,000 (Direct Cost: ¥980,000、Indirect Cost: ¥294,000); Fiscal Year 2008: ¥1,274,000 (Direct Cost: ¥980,000、Indirect Cost: ¥294,000)
• Keywords: 仕様記述 / 数理論理学 / 並列分散処理 / アルゴリズム工学 / 仕様記述・仕様検証

Research Abstract

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.

Research Products

• [Presentation] 安全性・余安全性に対する反例集合の獲得 (2008)
  • Author(s): 中野昌弘, 高井利憲
  • Organizer: 第5回システム検証の科学技術シンポジウム