現在の社会はソフトウェアへの依存度をますます高めており、その信頼性の向上が課題となっています。例えば、ウェブに関連したソフトウェアにおいては、プログラムの小さな誤りが、クロスサイトスクリプティングやSQLインジェクションなどの脆弱性の原因となり、情報漏洩などの深刻な問題を起こしています。本研究室では、ソフトウェアの信頼性を高めるための理論や技術を研究しています。特に、オートマトンや形式言語の理論に基づく検証技術の研究に注力しています。オートマトンは非常に単純な計算モデルですが、近年、様々な拡張が考えられ、ソフトウェア検証等の分野で応用が進んでいます。また、プログラミング言語の理論・実装や証明支援系の応用に関する研究も行っています。