| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2016-03-10 11:15 拡張Farkas補題の部分適用による非線形ループ不変式生成を用いたプログラム検証 ○柳澤真志・西田直樹・酒井正彦（名大）  SS2015-81 |
|
| 抄録 | （和） | ループ不変式を生成するための手法として，与えたテンプレートと事前条件と事後条件から得られる検証式をFarkas補題に基づき変換する手法が研究されている．Farkas補題に基づく変換では線形な多項式の不等式のみを原始論理式として含む論理式を等価変換する．それを変数や関数適用項の積を単項式とする多項式上に拡張した拡張Farkas補題が提案され，非線形なループ不変式を生成できる場合があることが示された．しかし，拡張Farkas補題を用いて生成したループ不変式がプログラム検証に有効かどうかについては議論されていない．本稿では，プロラム検証における拡張Farkas補題に基づくループ不変式の生成法の有効性を評価し，拡張Farkas補題を有効に利用する検証手法を提案する．具体的には，未知係数を含む複数の検証式の一部を拡張Farkas補題により変換し，それを充足する未知係数の割り当てを残りの検証式の未知係数に代入した後に恒真性を判定する． |
| （英） | To generate loop invariants, methods that, using Farkas' lemma, convert verification formulas obtained from a given template, a pre-condition, and a post-condtion of a program have been investigated. Farkas' lemma transforms formulas consisting of inequalities over linear polynomials into equivalent formulas. This lemma has been extended to deal with polynomials including non-linear monomials that may have function calls, and some examples that the extended Farkas' lemma succeeds in generating loop invariants having non-linear polynomials have been shown. However, it has not been discussed how useful the extended lemma is in verifying programs. In this paper, we evaluate the usefulness of a loop-invariant generation based on the extended Farkas' lemma, and propose a verification method that uses the extended lemma effectively. More precisely, using the extended lemma, we transform some of verification formulas that contain unknown coefficients for a given template, into another formula, and then we verify the validity of the formula obtained from the remaining formulas by applying an assignment for the unknown coefficients to satisfy the transformed formula. | |
| キーワード | （和） | プログラム検証 / ループ不変式 / ホーア論理 / Farkas補題 / / / / |
| （英） | program verification / loop invariant / Hoare logic / Farkas' lemma / / / / | |
| 文献情報 | 信学技報, vol. 115, no. 508, SS2015-81, pp. 31-36, 2016年3月. | |
| 資料番号 | SS2015-81 | |
| 発行日 | 2016-03-03 (SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2015-81 |
|
| 研究会情報 | |
| 研究会 | SS |
| 開催期間 | 2016-03-10 - 2016-03-11 |
| 開催地（和） | 沖縄県立宮古青少年の家 |
| 開催地（英） | |
| テーマ（和） | 一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2016-03-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | 拡張Farkas補題の部分適用による非線形ループ不変式生成を用いたプログラム検証 |
| サブタイトル（和） | |
| タイトル（英） | Program Verification Using Non-linear Loop Invariants Generated by Partially Applying an Extended Farkas' Lemma |
| サブタイトル（英） | |
| キーワード(1)（和/英） | プログラム検証 / program verification |
| キーワード(2)（和/英） | ループ不変式 / loop invariant |
| キーワード(3)（和/英） | ホーア論理 / Hoare logic |
| キーワード(4)（和/英） | Farkas補題 / Farkas' lemma |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 柳澤 真志 / Makishi Yanagisawa / ヤナギサワ マキシ |
| 第1著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 西田 直樹 / Naoki Nishida / ニシダ ナオキ |
| 第2著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 酒井 正彦 / Masahiko Sakai / サカイ マサヒコ |
| 第3著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya 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著者 所属（和/英） | (略称： ) (略称： ) |
| 講演者 | 第1著者 |
| 発表日時 | 2016-03-10 11:15:00 |
| 発表時間 | 25分 |
| 申込先研究会 | SS |
| 資料番号 | SS2015-81 |
| 巻番号（vol） | vol.115 |
| 号番号（no） | no.508 |
| ページ範囲 | pp.31-36 |
| ページ数 | 6 |
| 発行日 | 2016-03-03 (SS) |
[研究会発表申込システムのトップページに戻る]