ソフトウェアの安全性向上のための型理論の深化と応用
【研究分野】情報学基礎
【研究キーワード】
ソフトウェア検証 / 型システム / 高階モデル検査 / 資源使用法検証 / プログラム解析 / 型理論 / 述語抽象化 / メモリ使用法解析 / モデル検査 / 高階再帰スキーム / 資源使用法解析 / ツリーオートマトン
【研究成果の概要】
本研究では, ソフトウェアの信頼性向上のため, これまで研究代表者らが提案してきた型に基づくプログラム検証手法を実用レベルに引き上げるとともに, 検証手法の開拓を目標としていた. 前者の主な成果として, Cプログラムやセキュリティプロトコルの自動検証ツールの構築が挙げられる. また, 後者の主な成果として, 高階モデル検査のプログラム検証への応用を示すとともに, 世界初の高階モデル検査器の構築に成功した.
【研究代表者】