| 研究課題/領域番号 |
23220001
|
|---|
| 研究種目 |
基盤研究(S)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 東京大学 (2012-2015)
東北大学 (2011) |
|---|
研究代表者 |
小林 直樹 東京大学, 情報理工学(系)研究科, 教授 (00262155)
|
|---|
| 研究分担者 |
篠原 歩 東北大学, 大学院情報科学研究科, 教授 (00226151)
五十嵐 淳 京都大学, 大学院情報学研究科, 教授 (40323456)
海野 広志 筑波大学, 大学院システム情報工学研究科, 助教 (80569575)
|
|---|
| 連携研究者 |
寺内 多智弘 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70447150)
住井 英二郎 東北大学, 大学院情報科学研究科, 教授 (00333550)
松田 一孝 東北大学, 大学院情報科学研究科, 准教授 (10583627)
|
|---|
| 研究期間 (年度) |
2011-05-31 – 2016-03-31
|
| キーワード | 高階モデル検査 / プログラム検証 / データ圧縮 / 高階文法 / 型システム |
|---|
| 研究成果の概要 |
本研究の中心テーマである高階モデル検査とは、代表的なシステム検証手法であるモデル検査の拡張であり、2009年に研究代表者の小林によって初めて現実的な高階モデル検査アルゴリズムおよびプログラム検証への応用が見出された。本研究課題はその結果を受けて行った研究であり、高階モデル検査器の大幅な高速化、高階モデル検査に基づく全自動プログラム検証器の構築、高階モデル検査のデータ圧縮への応用（データをそれを生成する関数型プログラムの形に圧縮し、圧縮したままのデータ操作を実現）などの成果を得た。
|
| 自由記述の分野 |
プログラミング言語
|
