| 講演名 | 1995/7/14 プレスブルガー算術を用いたInfeasible Path検出の高速化技法 直井 邦彰, 高橋 直久, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本稿では,実行不可能経路(IFP)検出の際に用いられる,存在記号のみを持つプレスブルガー文(P文)の真偽判定を,効率よく行なう手法を提案する.従来のP文の判定法は,計算量のオーダが極めて大きく,実用的な時間内にIFP検出できない場合があった.提案手法では,Cooperの提案に基づき,存在記号のみを持つP文を高速に判定する手続きを定めた.本手法では,式に出現する変数を表す行列が三角化されるよう,数論の定理を用いてP文を変換する.本手法は,P文の同一アトムに同じ変数が頻繁に出現する場合,すなわち,IFP検出における経路条件に出現する変数の係数の値が大きい場合,特に有効である.このような場合,プロトタイプ・システムを用いた実験により、従来手法に比べて最高2000倍の速度向上を確認している. |
| 抄録(英) | A method based on a technique proposed by D.C.Cooper is proposed to efficiently decide whether a Presburger Sentence (P-sentence), which is used for detecting infeasible paths, is true or not. A P-sentence is converted to a conjunction form of divisibility relations. Next, a matrix which denotes variables on the relations is converted to a triangular matrix by using theorems in the number theory. The proposed method reduced the computation for the decision by triangulating the matrix. This paper also demonstrates that an implementation of the proposed method has reduced computation time by up to 2000 times. |
| キーワード(和) | 実行不可能経路 / プレスブルガー算術 / 数論 / プログラム解析 / 充足問題 / 決定問題 |
| キーワード(英) | infeasible path / Presburger arithmetic / number theory / program analysis / satisfiability problem / decision problem |
| 資料番号 | |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 1995/7/14(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | プレスブルガー算術を用いたInfeasible Path検出の高速化技法 |
| サブタイトル（和） | |
| タイトル（英） | Technique for reducing computation for detecting infeasible paths using Presburger arithmetic |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 実行不可能経路 / infeasible path |
| キーワード(2)（和/英） | プレスブルガー算術 / Presburger arithmetic |
| キーワード(3)（和/英） | 数論 / number theory |
| キーワード(4)（和/英） | プログラム解析 / program analysis |
| キーワード(5)（和/英） | 充足問題 / satisfiability problem |
| キーワード(6)（和/英） | 決定問題 / decision problem |
| 第 1 著者 氏名（和/英） | 直井 邦彰 / Kuniaki Naoi |
| 第 1 著者 所属（和/英） | NTTソフトウェア研究所:NTT武蔵野研究開発センタ NTT Software Laboratories |
| 第 2 著者 氏名（和/英） | 高橋 直久 / Naohisa Takahashi |
| 第 2 著者 所属（和/英） | NTTソフトウェア研究所:NTT武蔵野研究開発センタ NTT Software Laboratories |
| 発表年月日 | 1995/7/14 |
| 資料番号 | |
| 巻番号（vol） | vol.95 |
| 号番号（no） | 144 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |