形式手法では、プログラム言語のような形式言語（VDMやAlloyなど）を使って設計対象を厳密に表現します。AIの発達により、今後、仕様を厳密に表現することが重要になっていくと考えられます。
形式手法の一つで、数学の定理を証明するようにシステムの正当性を証明します。本研究室では定理証明言語（CoqやAgda）を用いたシステム検証について研究を行っています。
SAT(Satisfiability problem: 充足可能性問題)を効率的に解く方法を探求します。