Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic

• Shimizu Hiroaki

  IIM Corp.

• Hamaguchi Kiyoharu

  Osaka University

• Kashiwabara Toshinobu

  Osaka University

抄録

The use of a subset of first-order logic, called EUF, in model checking can be an effective abstraction technique for verifying larger and more complicated systems. The EUF model checking problem is, however, undecidable. In this paper, in order to guarantee the termination of state enumeration in the EUF-based model checking, we introduce a technique called term-height reduction. This technique is used to generate a finitely represented over-approximate set of states including all the reachable states. By checking a specified invariant property for this over-approximate set of states, we can safely assure that the invariant property always holds for the design, when verification succeeds. We also show some experimental results for a simple C program and a DSP design.

収録刊行物

• IPSJ Transactions on System LSI Design Methodology

  IPSJ Transactions on System LSI Design Methodology 3 105-117, 2010

  一般社団法人 情報処理学会

キーワード

• Electrical and Electronic Engineering
• Computer Science Applications

詳細情報

• CRID: 1390001205292645888
• NII論文ID: 110009599081
• NII書誌ID: AA12394951
• DOI: 10.2197/ipsjtsldm.3.105
• ISSN: 18826687
• Web Site: http://www.jstage.jst.go.jp/article/ipsjtsldm/3/0/3_0_105/_pdf
• 本文言語コード: en
• データソース種別:
  • JaLC
  • Crossref
  • CiNii Articles
  • KAKEN
• 抄録ライセンスフラグ: 使用不可