2006 Fiscal Year Annual Research Report
| Project/Area Number |
17300003
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
小林 直樹 東北大学, 大学院情報科学研究科, 教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
住井 英二郎 東北大学, 大学院情報科学研究科, 助教授 (00333550)
五十嵐 淳 京都大学, 大学院情報学研究科, 助教授 (40323456)
|
|---|
| Keywords | 型システム / プログラム解析 / 割り込み / 並行プログラム / 資源使用法解析 / プログラム等価性 / 双模倣 / 情報流解析 |
|---|
| Research Abstract |
ブログラムの安全性向上のために型理論に基づいたプログラム解析・検証・変換などの研究を行っている.本年度の主な研究成果は以下のとおり.
1.並行プログラムのための型システムの改良
型に基づいて並行プログラムのデッドロックなどの解析を行う手法を改良し,従来よりも精度よく解析できるようにした.また,プログラマが必要に応じて型宣言を行えるように型検査アルゴリズムを改良した.
さらに,割り込みが入った計算体系においてデッドロックが起きないことを検証するための型システムも考案した.
2.資源使用法解析の拡張
ファイルやメモリなどの計算資源が正しく使用されているかどうかを型を用いて検証する枠組みにおいて未解決であった,プログラムから推論された使用方法が仕様に適合することを検査するためのアルゴリズムを考案し,その正当性を証明した.
3.プログラムの等価性の検証手法の研究
高階関数・プロセスを持つ言語のプログラムの等価性や定義や証明のための一般的な手法がこれまで提案されておらず,個々の言語ごとにアドホックな手法が提案されていた.そこで,高階言語のための一般的な定義方法・証明手法として環境双模倣の枠組みを提案・定式化した.
4.割り込みの入った計算体系のためのデッドロック型とモデル検査の組み合わせによる情報流解析の手法の研究
ブログラムが機密情報を漏洩していないことを検証するための新しい手法として,型システムとモデル検査を融合した手法を考案した.これにより,モデル検査のみを使うよりも高速で,型のみによる手法と異なり,情報が漏れる場合の具体例を生成することができる.
|
