2010 Fiscal Year Self-evaluation 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 Tohoku University, 大学院・情報科学研究科, 教授 (00262155)
|
|---|
| Project Period (FY) |
2008 – 2010
|
| Keywords | ソフトウェア検証 / 型システム / 高階モデル検査 / 資源使用法検証 / プログラム解析 |
|---|
| Research Abstract |
交通システムや金融システム・原子力発電など重要な社会基盤の多くがコンピュータによって制御されている今日の高度情報化社会においては,ソフトウェアの信頼性向上が極めて重要かつ緊急の課題である.本研究では型システムに基づくソフトウェア検証の理論をさらに発展させ,研究代表者らがこれまでに取り組んできた並行プログラムの通信や同期の整合性,計算資源へのアクセス順序,セキュリティプロトコルなどの検証のための型理論を実用レベルにまで引き上げることを目標とする.また,そのような実用化に向けた研究を通じて,(1)ポインタや例外,割り込みなどの現実のプログラムに存在する複雑な言語機構を扱うための拡張,(2)検証精度と速度の向上,(3)モデル検査や定理証明など他の検証手法との融合,などの技術的課題 に取り組む
|
