Research Project
Grant-in-Aid for Scientific Research (A)
膨大なデータや通信を処理することが要請される近年のソフトウェアシステムにおいて,並行・並列処理を適切に行うことが重要となっている.しかし,並行・並列処理はシステムの実行順序や状態の可能性を爆発的に増大させるため,正しく動く並行・並列ソフトウェアシステムを構築するのは,並行・並列処理を行わない逐次実行的なソフトウェアを開発するよりも極めて困難となる.本研究は並行・並列処理を行うソフトウェアシステムの安全性を保証する上で重要となる時相的・状態依存的性質といったプログラムの詳細な性質の検証が可能なプログラム検証技術の実現およびその自動化を目指す.