電子商取引や交通インフラは、不具合発生による社会的な影響が大きいため高度な信頼性が要求されます。このため開発では不具合が混入しないように、人手による何重ものレビューと多種多様なテストが行われます。しかし、これら人手による作業には限界があり、不具合の可能性を完全に排除することはできません。本研究室ではソフトウェアが仕様通りに動作することをコンピュータによって厳密検証するシステムの研究を行っています。コンピュータプログラムは入力データから出力データを作る手続きを形式的な言語によって表現したものであり、その仕様と実装は数学的な命題と証明によって論理的に記述することができます。定理証明支援系は数学証明が厳密に正しいことを検証するシステムで、ソフトウェアプログラムが仕様通りに動作することを保証します。本研究室ではこの他に独居高齢者見守りシステム、医療データベース統合システムなどの研究開発を幅広く手がけています。

定理証明支援系によるソフトウェア検証の流れ