| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2012-01-26 14:15 関数呼び出しを持つプログラムの非線形ループ不変式の自動生成 ○鈴木英一・坂部俊樹・酒井正彦・草刈圭一朗・西田直樹（名大）  MSS2011-61 SS2011-46 |
|
| 抄録 | （和） | プログラム検証において，ループ実行中に常に成り立つ論理式である不変式が重要な役割を持っている．しかし，検証に有効なループ不変式を自動的に発見することは一般には困難である．本稿では，プログラム変数と関数呼び出し項に関する非線形の不等式で表されるループ不変式を，線形計画法などで利用されるFarkasの補題を拡張した定理に基づいて自動生成する手法を示す． |
| （英） | Finding loop invariants is one of the most important tasks in program verification. It is, however, difficult to automatically find meaningful loop invariants. In this report, we present a method for automatically generating loop invariants in the form of extended polynomial inequality, in which function instances may be included, over program variables. The method is based on the extended polynomial lemma which is improved to Farkas Lemma. | |
| キーワード | （和） | 静的解析 / プログラム検証 / 不変式生成 / 最弱事前条件 / / / / |
| （英） | static analysis / program verification / invariant generation / weakest preconditon / / / / | |
| 文献情報 | 信学技報, vol. 111, no. 406, SS2011-46, pp. 39-44, 2012年1月. | |
| 資料番号 | SS2011-46 | |
| 発行日 | 2012-01-19 (MSS, SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | MSS2011-61 SS2011-46 |
|
| 研究会情報 | |
| 研究会 | SS MSS |
| 開催期間 | 2012-01-26 - 2012-01-27 |
| 開催地（和） | 高知市文化プラザかるぽーと |
| 開催地（英） | Kochi City Culture-Plaza Cul-Port |
| テーマ（和） | 一般 |
| テーマ（英） | General topics |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2012-01-SS-MSS |
| 本文の言語 | 日本語 |
| タイトル（和） | 関数呼び出しを持つプログラムの非線形ループ不変式の自動生成 |
| サブタイトル（和） | |
| タイトル（英） | Automatic Generation of Non-linear Loop Invariants for Programs with Function Calls |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 静的解析 / static analysis |
| キーワード(2)（和/英） | プログラム検証 / program verification |
| キーワード(3)（和/英） | 不変式生成 / invariant generation |
| キーワード(4)（和/英） | 最弱事前条件 / weakest preconditon |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 鈴木 英一 / Eiichi Suzuki / スズキ エイイチ |
| 第1著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 坂部 俊樹 / Toshiki Sakabe / サカベ トシキ |
| 第2著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 酒井 正彦 / Masahiko Sakai / サカイ マサヒコ |
| 第3著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第4著者 氏名（和/英/ヨミ） | 草刈 圭一朗 / Keiichirou Kusakari / クサカリ ケイイチロウ |
| 第4著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第5著者 氏名（和/英/ヨミ） | 西田 直樹 / Naoki Nishida / ニシダ ナオキ |
| 第5著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2012-01-26 14:15:00 |
| 発表時間 | 30分 |
| 申込先研究会 | SS |
| 資料番号 | MSS2011-61, SS2011-46 |
| 巻番号（vol） | vol.111 |
| 号番号（no） | no.405(MSS), no.406(SS) |
| ページ範囲 | pp.39-44 |
| ページ数 | 6 |
| 発行日 | 2012-01-19 (MSS, SS) |
[研究会発表申込システムのトップページに戻る]