形式手法とは，システムの仕様を数学的に正確な形で記述し，その正しさを確認するための方法です．本研究室では，VDM や Alloy などを用いて，曖昧さのない仕様の書き方や，その解析方法を研究しています． 生成AIの普及により，システムの動作を「なんとなく正しい」ではなく，「確実に正しい」と言えるようにする技術の重要性が高まっています．
定理証明手法とは，仕様が正しいことをコンピュータ上で証明する方法です．本研究室では，Coq や Lean といったツールを用いて，プログラムやシステムの正しさを厳密に確認する研究を行っています． このような技術は，バグが許されないような高信頼なシステムの開発に役立ちます．
生成AIを使ったプログラミング（AIコーディング）が広がっていますが，「どう使えばよいか」「どうすれば安全に使えるか」はまだ十分に整理されていません．本研究室では，AIによるコード生成を工学的に分析し，開発プロセスへの取り入れ方や品質の保ち方に注目していきます． AIと人間が協力してソフトウェアを開発する，新しい開発スタイルの確立を目指しています．
形式的意味論とは，自然言語の意味を数学的に記述する分野です．文がどのような意味を持つのかを，形式的に表現します． 近年の生成AIは高度な言語処理を実現していますが，その振る舞いを厳密に説明・保証する理論はまだ十分ではありません．本研究室では，自然言語の意味の解析を中心に，プログラムや回路の振る舞いも形式的に記述・解析する研究を行っています．