| 研究課題/領域番号 |
15K00027
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
龍田 真 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | ソフトウェア検証 / 数理論理 / 分離論理 |
|---|
| 研究実績の概要 |
一般的帰納的定義}の条件で次の(1)(2)を満たすものを発見し、その性質を証明する研究を行った。(1) 記号ヒープ体系にその条件下の一般的帰納的定義を追加しても、エンテイルメントの真偽が決定可能である, (2) リストセグメントなどのよく使用される基本的なデータ構造が記述できる. 本研究の実用的な意義は、メモリーエラーを自動定理証明により検証する方法に対して、リストセグメントのようなよく使われる基本的なデータ構造を扱うプログラムを対話的入力なしに全自動で検証できる方法をはじめて与えることである。
平成２７年度の実績は次のようである。論文 Iosif et al 2013の証明の条件を吟味し、その条件を緩めて、データフィールドを扱えるようにした。単項二階論理への翻訳を可能とする条件として、単項帰納的定義の条件を発見した。この条件を用いて、エンテイルメントの決定手続きを設計し決定可能性定理を証明した。このシステムのパソコンへ実装した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
平成２７年度にやるように当初計画していたことは全て達成できた。また、bounded treewidth の条件下で循環証明体系を構築し、その決定可能性を証明した。また、その実装も開始した。以上から進捗状況はよいといえる。
|
| 今後の研究の推進方策 |
(1) 平成27年度に構成した検証システムの決定手続きのパソコン上への実装を完成する。実装は、O'Hearn らのグループの 2005, 2006年の論文をはじめとする分離論理の検証システムの実装の論文のアイデアを参考にして、検証システムのプロトタイプを作成する。(2) 実装した検証システムに, ベンチマークなどを走らせ実験する。(3) 平成27年度に発見した条件と理論をさらに洗練する。
検証システムの実装および実験のために、平成28年度には研究補助者を週１日雇用する。最新の状況を捉えるために、成果発表とは別に年１回トップ会議に出席して情報収集する。国内の関連した研究を行っているグループを訪問し、途中の成果を発表し、研究討論を行ってフィードバックを得る。研究成果を権威ある国際会議で発表し研究討論を行う。
|
| 次年度使用額が生じた理由 |
実装および実験のための研究補助の支出のため追加交付を受けたが、発表旅費が予定より少なかったため次年度使用額が生じた。
|
| 次年度使用額の使用計画 |
理論研究が予定よりよく進み、また実験から得るデータが予想より研究に役立つことがわかったため、実装とそのシステムによる実験にも重きを置くこととし、そのために研究員または研究補助員を雇用する。その他の点については当初予定通り進める。
|
