| 研究課題/領域番号 |
20240001
|
|---|
| 研究種目 |
基盤研究(A)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
小林 直樹 東北大学, 情報科学研究科, 教授 (00262155)
|
|---|
| 研究分担者 |
五十嵐 淳 (五十風 淳) 京都大学, 大学院・情報学研究科, 准教授 (40323456)
住井 英二郎 東北大学, 大学院・情報科学研究科, 准教授 (00333550)
松田 一孝 東北大学, 大学院・情報科学研究科, 助教 (10583627)
寺内 多智弘 東北大学, 大学院・情報科学研究科, 助教 (70447150)
|
|---|
| 研究期間 (年度) |
2008 – 2010
|
| 研究課題ステータス |
完了 (2011年度)
|
| 配分額 *注記 |
49,270千円 (直接経費: 37,900千円、間接経費: 11,370千円)
2011年度: 10,920千円 (直接経費: 8,400千円、間接経費: 2,520千円)
2010年度: 13,520千円 (直接経費: 10,400千円、間接経費: 3,120千円)
2009年度: 10,920千円 (直接経費: 8,400千円、間接経費: 2,520千円)
2008年度: 13,910千円 (直接経費: 10,700千円、間接経費: 3,210千円)
|
|---|
| キーワード | ソフトウェア検証 / 型システム / 高階モデル検査 / 資源使用法検証 / プログラム解析 / 型理論 / 述語抽象化 / メモリ使用法解析 / モデル検査 / 高階再帰スキーム / 資源使用法解析 / ツリーオートマトン |
|---|
| 研究概要 |
本研究では, ソフトウェアの信頼性向上のため, これまで研究代表者らが提案してきた型に基づくプログラム検証手法を実用レベルに引き上げるとともに, 検証手法の開拓を目標としていた. 前者の主な成果として, Cプログラムやセキュリティプロトコルの自動検証ツールの構築が挙げられる. また, 後者の主な成果として, 高階モデル検査のプログラム検証への応用を示すとともに, 世界初の高階モデル検査器の構築に成功した.
|
