2007 Fiscal Year Annual Research Report
| Project/Area Number |
17300003
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
小林 直樹 Tohoku University, 大学院・情報科学研究科, 教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
住井 英二郎 東北大学, 大学院・情報科学研究科, 准教授 (00333550)
五十嵐 淳 京都大学, 大学院・情報学研究科, 准教授 (40323456)
寺内 多智弘 東北大学, 大学院・情報科学研究科, 助教 (70447150)
|
|---|
| Keywords | 型システム / プログラム解析 / デッドロック / 並行プログラム / 資源使用法解析 / プログラム等価性 / 線形最適化問題 / 情報流解析 |
|---|
| Research Abstract |
本研究ではソフトウェアを実行前に検証するための型理論の研究を行っている.
本年度は,並行プログラムの検証のための型システムに関して以下の成果が得られた.
1.並行プログラムの停止性の検証のための型システムDengとSangiorgiによる並行プログラムの停止性の検証のための型システムを改良し,並行プログラムの停止性の自動検証を可能にするための型推論 アルゴリズムを考案した.また,それらのアルゴリズムをプログラム検証器TyPiCalに実装した.
2.使用法宣言を許す並行プログラムの型システムの決定不能性について並行プログラムの型システムにおいて使用法表現と呼ばれる型の宣言を許すと型システムが決定不能になることを証明した.これにより,使用法宣言を制限する必要性が理論的に確認された.
3.通信チャネルのキューの長さの上限の解析通信チャネルのキューの長さの上限を推論する問題を型システムを用いて線形最適化問題に還元した.これにより,種々の最適化や競合条件の解析が可能となった.
4.デッドロックの原因特定のための型エラースライシング型エラースライシングの概念をデッドロック解析のための型システムに適用することにより,デッドロックの原因個所をプログラムスライスとして取出す手法を考案し,実装した.
5.割り込みの入った計算体系におけるデッドロックの解析割り込みの入った計算体系においてデッドロックの有無を静的に解析するための型システムを考案した.
|
