開学以来の研究教育活動と「検証進化可能電子社会」プロジェクトなどのプロジェクト研究を通じて,JAISTにはソフトウェア検証に関する国内最強の研究グループが形成されてきた。ソフトウェア検証研究センターは,このグループの活動をより発展させ,世界トップレベルの研究を展開することを目指して,2010年4月に創設された.
JAISTでは現在まで,ソフトウェア検証に関して,次のような多彩なテーマの研究を行い成果を上げてきた.
- 代数的論理学、部分構造論理、様相論理
- 構成的数学,直観主義論理,逆数学
- 代数的ゲーム理論, 代数的システム生物学
- 形式仕様言語CafeOBJとそれを用いた仕様検証法
- 対話的定理証明とモデル検査を統合した検証法
- ハイブリッドシステム理論とその設計・検証アルゴリズムの高速化法
- 大規模webアプリケーションのセキュリティ解析、組込みシステムにおけるDSP デコーダの丸め誤差自動解析、停止性自動証明
- リアルタイムオペレーティングシステムの形式検証法と支援ツール
以上の成果に基づき,ソフトウェア検証研究センターでは,次のようなテーマに関する研究を総合的に展開していく予定である.
- 検証の論理: 必然性や証明可能性を議論できる論理など,次世代の検証技術の基盤となる新しい論理.
- 検証の機構:モデル検査,定理証明,書換などの様々な検証機構とプログラムコード検証.
- モデル化・形式仕様言語: 実世界の問題やシステムをモデル化し形式仕様として定式化するための言語と、問題・要求・仕様・設計の検証法.
- 実時間・ハイブリッドシステム: 実時間・並行・ハイブリッド・ネットワークシステムやプロトコルの検証技術.