現代社会において、人々は日常的にスマートフォンやコンピュータを私生活や仕事に用いており、普段意識されない交通・金融・医療・エネルギーといった社会基盤もコンピュータにより制御されている。したがって、コンピュータを動かすプログラムであるソフトウェアの信頼性を確保し、効率性を向上させることは、社会の安定と円滑な機能の維持にとって重要な課題となっている。

本研究室では、形式論理やプログラム理論といった基礎理論に基づいた高信頼・高効率ソフトウェア構成技術の研究を行っている。特に、与えられたプログラムがその仕様を満たすことを数学的に厳密に保証するための技術であるプログラム検証や、仕様からそれを満たすプログラムを生成するための技術であるプログラム合成の研究・開発を進めている。例えば、関数型プログラミング言語 OCaml に検証・合成ツールを統合することによって、高信頼・高効率プログラムの開発を促進することを目指した RCaml や、多様な検証・合成問題を述語制約や不動点論理式として表現して解くことができるソルバである PCSat や MuVal, MuCyc, MuStrat の研究・開発を行っている。また、これらのツールの基礎となるプログラム理論や型理論、制約解消・最適化の理論、不動点論理とその演繹体系についても研究を行っている。