2010 Fiscal Year Final Research Report
Advancement and Application of Type Theory for Improving Software Safety
| Project/Area Number |
20240001
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (A)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
KOBAYASHI Naoki 東北大学, 大学院・情報科学研究科, 教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
IGARASHI Atsushi 京都大学, 大学院・情報学研究科, 准教授 (40323456)
SUMII Eijiro 東北大学, 大学院・情報科学研究科, 准教授 (00333550)
MATSUDA Kazutaka 東北大学, 大学院・情報科学研究科, 助教 (10583627)
TERAUCHI Tachio 東北大学, 大学院・情報科学研究科, 助教 (70447150)
|
|---|
| Project Period (FY) |
2008 – 2010
|
| Keywords | ソフトウェア検証 / 型システム / 高階モデル検査 / 資源使用法検証 / プログラム解析 |
|---|
| Research Abstract |
This research project aimed to improve the reliability of computer software, by refining type-based program verification methods we have studied before, and also by inventing new program verification techniques. As the former study, we have constructed verification tools for C programs and cryptographic protocols. As the latter study, we have shown novel applications of higher-order model checking to program verification, and constructed the first higher-order model checker in the world.
|
