| 研究課題/領域番号 |
15H05706
|
|---|
| 研究種目 |
基盤研究(S)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
情報学基礎理論
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
小林 直樹 東京大学, 大学院情報理工学系研究科, 教授 (00262155)
|
|---|
| 研究分担者 |
篠原 歩 東北大学, 情報科学研究科, 教授 (00226151)
佐藤 亮介 九州大学, システム情報科学研究院, 助教 (10804677)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| 研究期間 (年度) |
2015-05-29 – 2020-03-31
|
| 研究課題ステータス |
完了 (2020年度)
|
| 配分額 *注記 |
193,960千円 (直接経費: 149,200千円、間接経費: 44,760千円)
2019年度: 38,610千円 (直接経費: 29,700千円、間接経費: 8,910千円)
2018年度: 37,960千円 (直接経費: 29,200千円、間接経費: 8,760千円)
2017年度: 39,780千円 (直接経費: 30,600千円、間接経費: 9,180千円)
2016年度: 41,600千円 (直接経費: 32,000千円、間接経費: 9,600千円)
2015年度: 36,010千円 (直接経費: 27,700千円、間接経費: 8,310千円)
|
|---|
| キーワード | 高階モデル検査 / プログラム検証 / データ圧縮 / 型システム / 関数型プログラム / 高階不動点論理 / 不動点論理 / 高階文法 / 確率付き文法 / 高階論理 / 共通型 |
|---|
| 研究成果の概要 |
本研究では、代表者らがこれまで発展させてきた高階モデル検査の理論およびプログラム検証等への応用を発展させることを目的とした。理論面では、高階文法の反復補題についての40年以上ぶりの進展を得るとともに、異なる2種類の高階モデル検査であるHORSモデル検査とHFLモデル検査の間の関係を明らかにするなど、大きな進展が得られた。また応用面でも、高階モデル検査器およびプログラム自動検証器の大幅な高速化、検証できる性質の拡大、高階データ圧縮のための算術符号化などの成果が得られた。
|
| 研究成果の学術的意義や社会的意義 |
上述の成果は、代表者の専門であるプログラム検証などプログラミング言語分野・ソフトウェアの基礎理論のみならず、反復補題に関する40年以上ぶりの進展など、形式言語理論、計算量理論、データ圧縮など周辺の様々な学問分野に新たな知見をもたらすものであり、学術的意義が大きい。また、プログラムの自動検証技術を大きく進展させ、社会基盤を支えるコンピュータシステムの安全性向上に寄与するという社会的意義も大きい。
|
| 評価記号 |
検証結果 (区分)
A+
|
評価記号 |
評価結果 (区分)
A+: 当初目標を超える研究の進捗があり、期待以上の成果が見込まれる
|
