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

スポンサーリンク

概要

• 論文の詳細を見る

• 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 EUFbased 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.

• 一般社団法人情報処理学会の論文
• 2010-02-15

著者

• Kiyoharu Hamaguchi

  Osaka University

• Toshinobu Kashiwabara

  Osaka University

• Hiroaki Shimizu

  Presently with IIM Corp.

関連論文

• Checker Generation of Assertions with Local Variables for Model Checking
• Approximate Model Checking Using a Subset of First-order Logic
• Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic
• Symbolic Discord Computation for Efficient Analysis of Message Sequence Charts

スポンサーリンク