• プログラムの効率の改善や形式的検証に関する研究を行っている。短期間で記述したプログラムは実行時間やメモリ使用量について非効率的であることが多いが、この問題に対し、プログラム変換によって機械的に改善する手法の開発に取り組んでいる。また、大規模なプログラムはその複雑さから予期せぬバグを含みやすいが、この問題に対しては、プログラム検証やモデル検査とよばれる数学的手法によって実行前に網羅的に検証する研究も進めている。

通常のソフトウェア開発では有限個のテストを通じて動作確認が行われるが、モデル検査器や定理証明支援系などのツールを用いることで、無限個の入力に対して動作が保証されたプログラムの作成を実現できる。

• プログラミング言語
• 高信頼ソフトウェア
• モデル検査
• 形式検証
• 証明支援系