| 配分額 *注記 |
12,160千円 (直接経費: 10,900千円、間接経費: 1,260千円)
2007年度: 5,460千円 (直接経費: 4,200千円、間接経費: 1,260千円)
2006年度: 3,100千円 (直接経費: 3,100千円)
2005年度: 3,600千円 (直接経費: 3,600千円)
|
|---|
| 研究概要 |
本研究の目的は,ソフトウェアの信頼性向上のため,型理論などの数理科学的手法に基づいたプログラムの検証手法を発展させることにあった.特に,これまでの申請者らによる検証手法を改良・発展させ,現実のプログラムの検証を可能にすることに主眼をおいた.
3年間の主要な成果は以下のとおり.以下のいずれの研究においても実際にプログラム検証器のプロトタイプを作成し有効性を確認している.
1.関数型プログラムの検証手法
以前から,ファイルやメモリなどの計算資源を正しいプロトコルでアクセスするかどうかを検証するための資源使用法解析について研究を行っていたが,例外処理機構を扱っていないなど,実際のプログラミング言語とは開きがあった.そこで,従来の我々の検証手法を拡張し,例外処理機構に対応できるようにした.また,従来の型を用いた自動検証手法では,一般に解析精度が粗かったため,依存型の自動推論手法を考案することにより,精度のよい解析を自動で行えるようにした.
2.並行プログラムの検証手法
以前からπ計算を対象として,デッドロックなどの自動解析手法を研究していたが,実用化する上での解析精度,実際の言語が提供するプリミティブとの開きなどがあった.そこで,前者の問題をモデル検査などとの融合によって改善した.また,後者の問題に対処するため,ポインタや割り込みなどが入った言語に対する解析手法も考案した.
3.情報流解析
プログラムが機密情報を漏らさないかどうかを検証する情報流解析について研究を行った.従来から型を用いた情報流解析手法は提案されていたが精度が問題だったため,本研究ではモデル検査手法と融合させることにより,高速かつ精度のよい解析を可能にした.
|
