| 講演抄録／キーワード |
| 講演名 |
2007-11-20 11:20
第一階述語論理のサブクラスに対する項の高さ縮減を用いた不変条件の近似的検証アルゴリズム
○清水博章・浜口清治・柏原敏伸（阪大） |
| 抄録 |
（和） |
自動的にハードウェア設計の形式的検証を行う手法にモデルチェッキング技術があるが，モデルチェッキングには，扱うシステムが大規模になると状態数が爆発してしまい，計算量的に適用できないという問題がある．計算量を軽減するための1つの方法として，EUFと呼ばれる第一階述語論理のサブクラスを用いてシステムを抽象化する手法が提案されているが，EUFを用いたモデルチェッキングは一般に決定不能であることが知られている．本稿では，EUFの項の高さに上限を与えることで，現れうる項の形を制限し，状態集合の数え上げを終了させる手法を提案する．また数え上げた状態集合に対して，指定した不変条件の成立を保証できる近似アルゴリズムを提案する．さらに，アルゴリズムを簡単な回路設計に適用した例を示す． |
| （英） |
Model checking technique, which is a method to verify systems automatically, have attracted attentions. Model checking, however, cannot be applied to systems which are large or complicated. To handle this problem, abstraction techniques using a subset of first-order logic, called EUF, have been proposed, but a model checking using EUF is generally undecidable. In this report, we introduce a method to terminate state enumeration by using term-height reduction. Finally we show an overapproximate algorithm which can check if a designated invariant always holds for the system. Furthermore, we show an example of application of our algorithm to simple hardware designs. |
| キーワード |
（和） |
モデルチェッキング / 第一階述語論理 / 抽象化 / 不変条件 / / / / |
| （英） |
model checking / first-order logic / abstraction / invariant / / / / |
| 文献情報 |
信学技報, vol. 107, pp. 19-24, 2007年11月. |
| 資料番号 |
|
| 発行日 |
2007-11-13 (VLD, DC) |
| ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
| PDFダウンロード |
|
| 研究会情報 |
| 研究会 |
VLD CPSY RECONF DC IPSJ-SLDM IPSJ-ARC |
| 開催期間 |
2007-11-20 - 2007-11-22 |
| 開催地（和） |
北九州国際会議場 |
| 開催地（英） |
Kitakyushu International Conference Center |
| テーマ（和） |
デザインガイア2007 ―VLSI設計の新しい大地を考える研究会― |
| テーマ（英） |
Design Gaia 2007 ---A New Frontier in VLSI Design--- |
| 講演論文情報の詳細 |
| 申込み研究会 |
IPSJ-SLDM |
| 会議コード |
2007-11-VLD-CPSY-RECONF-DC-IPSJ-SLDM-IPSJ-ARC |
| 本文の言語 |
日本語 |
| タイトル（和） |
第一階述語論理のサブクラスに対する項の高さ縮減を用いた不変条件の近似的検証アルゴリズム |
| サブタイトル（和） |
|
| タイトル（英） |
An Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic |
| サブタイトル（英） |
|
| キーワード(1)（和/英） |
モデルチェッキング / model checking |
| キーワード(2)（和/英） |
第一階述語論理 / first-order logic |
| キーワード(3)（和/英） |
抽象化 / abstraction |
| キーワード(4)（和/英） |
不変条件 / invariant |
| キーワード(5)（和/英） |
/ |
| キーワード(6)（和/英） |
/ |
| キーワード(7)（和/英） |
/ |
| キーワード(8)（和/英） |
/ |
| 第1著者 氏名（和/英/ヨミ） |
清水 博章 / Hiroaki Shimizu / シミズ ヒロアキ |
| 第1著者 所属（和/英） |
大阪大学 (略称： 阪大)
Osaka University (略称： Osaka Univ.) |
| 第2著者 氏名（和/英/ヨミ） |
浜口 清治 / Kiyoharu Hamaguchi / ハマグチ キヨハル |
| 第2著者 所属（和/英） |
大阪大学 (略称： 阪大)
Osaka University (略称： Osaka Univ.) |
| 第3著者 氏名（和/英/ヨミ） |
柏原 敏伸 / Toshinobu Kashiwabara / カシワバラ トシノブ |
| 第3著者 所属（和/英） |
大阪大学 (略称： 阪大)
Osaka University (略称： Osaka Univ.) |
| 第4著者 氏名（和/英/ヨミ） |
/ / |
| 第4著者 所属（和/英） |
(略称： )
(略称： ) |
| 第5著者 氏名（和/英/ヨミ） |
/ / |
| 第5著者 所属（和/英） |
(略称： )
(略称： ) |
| 第6著者 氏名（和/英/ヨミ） |
/ / |
| 第6著者 所属（和/英） |
(略称： )
(略称： ) |
| 第7著者 氏名（和/英/ヨミ） |
/ / |
| 第7著者 所属（和/英） |
(略称： )
(略称： ) |
| 第8著者 氏名（和/英/ヨミ） |
/ / |
| 第8著者 所属（和/英） |
(略称： )
(略称： ) |
| 第9著者 氏名（和/英/ヨミ） |
/ / |
| 第9著者 所属（和/英） |
(略称： )
(略称： ) |
| 第10著者 氏名（和/英/ヨミ） |
/ / |
| 第10著者 所属（和/英） |
(略称： )
(略称： ) |
| 第11著者 氏名（和/英/ヨミ） |
/ / |
| 第11著者 所属（和/英） |
(略称： )
(略称： ) |
| 第12著者 氏名（和/英/ヨミ） |
/ / |
| 第12著者 所属（和/英） |
(略称： )
(略称： ) |
| 第13著者 氏名（和/英/ヨミ） |
/ / |
| 第13著者 所属（和/英） |
(略称： )
(略称： ) |
| 第14著者 氏名（和/英/ヨミ） |
/ / |
| 第14著者 所属（和/英） |
(略称： )
(略称： ) |
| 第15著者 氏名（和/英/ヨミ） |
/ / |
| 第15著者 所属（和/英） |
(略称： )
(略称： ) |
| 第16著者 氏名（和/英/ヨミ） |
/ / |
| 第16著者 所属（和/英） |
(略称： )
(略称： ) |
| 第17著者 氏名（和/英/ヨミ） |
/ / |
| 第17著者 所属（和/英） |
(略称： )
(略称： ) |
| 第18著者 氏名（和/英/ヨミ） |
/ / |
| 第18著者 所属（和/英） |
(略称： )
(略称： ) |
| 第19著者 氏名（和/英/ヨミ） |
/ / |
| 第19著者 所属（和/英） |
(略称： )
(略称： ) |
| 第20著者 氏名（和/英/ヨミ） |
/ / |
| 第20著者 所属（和/英） |
(略称： )
(略称： ) |
| 講演者 |
第1著者 |
| 発表日時 |
2007-11-20 11:20:00 |
| 発表時間 |
25分 |
| 申込先研究会 |
IPSJ-SLDM |
| 資料番号 |
VLD2007-73, DC2007-28 |
| 巻番号（vol） |
vol.107 |
| 号番号（no） |
no.334(VLD), no.337(DC) |
| ページ範囲 |
pp.19-24 |
| ページ数 |
6 |
| 発行日 |
2007-11-13 (VLD, DC) |
|