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