| 研究課題/領域番号 |
23220001
|
|---|
| 研究種目 |
基盤研究(S)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 東京大学 (2012-2015)
東北大学 (2011) |
|---|
研究代表者 |
小林 直樹 東京大学, 情報理工学(系)研究科, 教授 (00262155)
|
|---|
| 研究分担者 |
篠原 歩 東北大学, 大学院情報科学研究科, 教授 (00226151)
五十嵐 淳 京都大学, 大学院情報学研究科, 教授 (40323456)
海野 広志 筑波大学, 大学院システム情報工学研究科, 助教 (80569575)
|
|---|
| 連携研究者 |
寺内 多智弘 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70447150)
住井 英二郎 東北大学, 大学院情報科学研究科, 教授 (00333550)
松田 一孝 東北大学, 大学院情報科学研究科, 准教授 (10583627)
|
|---|
| 研究期間 (年度) |
2011-05-31 – 2016-03-31
|
| 研究課題ステータス |
完了 (2015年度)
|
| 配分額 *注記 |
137,540千円 (直接経費: 105,800千円、間接経費: 31,740千円)
2015年度: 28,990千円 (直接経費: 22,300千円、間接経費: 6,690千円)
2014年度: 29,120千円 (直接経費: 22,400千円、間接経費: 6,720千円)
2013年度: 28,080千円 (直接経費: 21,600千円、間接経費: 6,480千円)
2012年度: 28,730千円 (直接経費: 22,100千円、間接経費: 6,630千円)
2011年度: 22,620千円 (直接経費: 17,400千円、間接経費: 5,220千円)
|
|---|
| キーワード | 高階モデル検査 / プログラム検証 / データ圧縮 / 高階文法 / 型システム / 関数型プログラム / 関数型言語 / 高階再帰スキーム / 型理論 |
|---|
| 研究成果の概要 |
本研究の中心テーマである高階モデル検査とは、代表的なシステム検証手法であるモデル検査の拡張であり、2009年に研究代表者の小林によって初めて現実的な高階モデル検査アルゴリズムおよびプログラム検証への応用が見出された。本研究課題はその結果を受けて行った研究であり、高階モデル検査器の大幅な高速化、高階モデル検査に基づく全自動プログラム検証器の構築、高階モデル検査のデータ圧縮への応用（データをそれを生成する関数型プログラムの形に圧縮し、圧縮したままのデータ操作を実現）などの成果を得た。
|
| 評価記号 |
検証結果 (区分)
A
|
評価記号 |
評価結果 (区分)
A: 当初目標に向けて順調に研究が進展しており、期待どおりの成果が見込まれる
|
