| 研究課題/領域番号 |
15K00027
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎理論
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
龍田 真 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
|
|---|
| 連携研究者 |
木村 大輔 東邦大学, 理学部情報科学科, 講師 (90455197)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2017-03-31
|
| 研究課題ステータス |
完了 (2016年度)
|
| 配分額 *注記 |
4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円)
2017年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2016年度: 2,470千円 (直接経費: 1,900千円、間接経費: 570千円)
2015年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
|
|---|
| キーワード | 分離論理 / ソフトウェア検証 / 記号ヒープ / 帰納的定義 / 数理論理 |
|---|
| 研究成果の概要 |
(1) 単項帰納的定義と暗黙存在のある分離論理のエンテイルメントの決定可能 性を証明した。この体系は、有界木幅分離論理 SLRDbtw から、暗黙存在変数を追加し、帰納的定義を単項に制限することにより得られる。(2) 単項帰納的定義をもつ記号ヒープのエンテイルメント判定器を実装した。効率的実装のためのアイデアとして、木のノード間の同値関係に関する最適化を説明した。(3) 相互再帰手続きをもつポインタープログラムにホーア論理と分離論理の拡張した体系の完全性を証明した。(4) プレスバーガー算術と帰納的定義をもつ分離論理における記号ヒープの充足可能性問題を解いた。
|
