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 Tohoku University, 情報科学研究科, 教授 (00262155)
|
Co-Investigator(Kenkyū-buntansha) |
IGARASHI Atsushi 京都大学, 大学院・情報学研究科, 准教授 (40323456)
SUMII Eijiro 東北大学, 大学院・情報科学研究科, 准教授 (00333550)
MATSUDA Kazutaka 東北大学, 大学院・情報科学研究科, 助教 (10583627)
TERAUCHI Tachio 東北大学, 大学院・情報科学研究科, 助教 (70447150)
|
Project Period (FY) |
2008 – 2010
|
Project Status |
Completed (Fiscal Year 2011)
|
Budget Amount *help |
¥49,270,000 (Direct Cost: ¥37,900,000、Indirect Cost: ¥11,370,000)
Fiscal Year 2011: ¥10,920,000 (Direct Cost: ¥8,400,000、Indirect Cost: ¥2,520,000)
Fiscal Year 2010: ¥13,520,000 (Direct Cost: ¥10,400,000、Indirect Cost: ¥3,120,000)
Fiscal Year 2009: ¥10,920,000 (Direct Cost: ¥8,400,000、Indirect Cost: ¥2,520,000)
Fiscal Year 2008: ¥13,910,000 (Direct Cost: ¥10,700,000、Indirect Cost: ¥3,210,000)
|
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.
|
Report
(5 results)
Research Products
(50 results)