研究分担者 |
五十嵐 淳 京都大学, 大学院・情報学研究科, 准教授 (40323456)
住井 英二郎 東北大学, 大学院・情報科学研究科, 准教授 (00333550)
松田 一孝 東北大学, 大学院・情報科学研究科, 助教 (10583627)
寺内 多智弘 東北大学, 大学院・情報科学研究科, 助教 (70447150)
|
研究概要 |
本研究では, ソフトウェアの信頼性向上のため, これまで研究代表者らが提案してきた型に基づくプログラム検証手法を実用レベルに引き上げるとともに, 検証手法の開拓を目標としていた. 前者の主な成果として, Cプログラムやセキュリティプロトコルの自動検証ツールの構築が挙げられる. また, 後者の主な成果として, 高階モデル検査のプログラム検証への応用を示すとともに, 世界初の高階モデル検査器の構築に成功した.
|