コンピュータソフトウェア分野では，数学的な厳密さを以てその正しさが保証されたプログラムを作成することを究極の目標とし，ソフトウェアに関する数学的な基礎理論(プログラム理論)を構築する研究を行っている. 最近の主要テーマは以下の通りである．
これらの研究に共通するのは，「論理」をキーワードとしているという点であり，論理学に基づいた厳密な手法をソフトウェアの世界に適用するという考え方である．
最近発表したポスター 五十嵐の最近の研究論文リスト 末永の最近の研究論文リスト 和賀の最近の研究論文リスト
プログラムを「動けば良い」という観点だけから見る人にとって，基礎理論は必要ないかも知れない．実際，簡単なプログラムであれば，特に頭を使わなくても手を動かすだけで自然に書けてしまうことも多い．しかし，書いたプログラムがきちんと意図通りに動くことが必要な場合，それでは済まない.現在のソフトウェア開発では，プログラムを運用する前にテストを行うことでプログラムが正しく動くかを検査しているが，テストだけではカバーできる範囲に限界があるため不十分である．自動車や航空機の制御プログラム，金融機関の基幹システム，ブロックチェーンなど社会的に重要度の高いプログラム，デバイスドライバなどの事前にテストができない(行いにくい)プログラムでは，正しく動くことを，プログラムの運用前に予め厳密に保証する手法が求められている．そのような要請に答えるためには，ただプログラムを書けば良いのではなく，プログラムがどのように動いてほしいか， という要求仕様を明確にし，さらに，プログラムがその仕様を満たすことの保証を付ける必要がある．書かれたプログラムが仕様を満たしているかを確かめることを プログラム検証 という．
プログラム検証のための基本的な技術には型理論，モデル検査，プログラム論理などいくつか代表的なものがあり，それぞれ長所・短所がある．これまでは，型理論という手法(コンパイラが行う型検査の基礎理論でもあり，予め決められたエラーを検出するのに向いている)に重きを置いてきたが，最近はその他の技術との融合も目指している．
この分野では例えば以下のような研究テーマに取り組んでいる．
篩型 (refinement types) とは，int や string といった単純な型を拡張して「偶数である」「長さが10より小さい文字列」といった付加的な性質が表せるようにした型であり，関数型プログラムの検証のために盛んに研究・利用されている．しかし，篩型とC言語のようなポインタを通じた変数への破壊的代入がある言語の相性は悪く，そのままでは使えない．我々は分割可能所有権(fractional ownership)と呼ばれる，変数への読み書きと変数のエイリアスを制御する仕組みと篩型を組み合わせた，ポインタを使うプログラムの自動検証の理論と検証器の実装に取り組んでいる．
ハイブリッドシステムとは，制御にソフトウェアが関わっている飛行機等， 力学・電気系の連続量で記述される動作と，ソフトウェアの離散量で記述される動作によって全体の動作が実現されるシステムである．本研究ではソフトウェアテストの手法をハイブリッドシステムに拡張することでハイブリッドシステムを検証することを目指している．
モデル検査器は検証の過程でヒューリスティクスを用いることが多く，その良し悪しがモデル検査器の性能を大きく左右することが多い．本研究では強化学習を用いることにより，より高速なヒューリスティクスを発見することを目指している．
スマートコントラクトは，ブロックチェーン上で自動的に決済などを行うためのプログラムである．スマートコントラクトは見た目単純なものが多いが，バグが入ると経済的な大きな損失が発生してしまう(実際に発生している)．我々は Tezos というブロックチェーン上のスマートコントラクト言語 Michelson を対象としたプログラム検証器を開発しながら，スマートコントラクトの検証技法の研究を行っている．
量子プログラムは，量子ビットと呼ばれる1/0が重ね合わせ状態にある特殊なビットを使った量子アルゴリズムを記述するプログラムで，量子回路モデルや，理論的な分野では関数型の量子プログラミング言語などが研究されている．量子プログラムは，量子ビットの複製不可能性や量子コンピュータのアーキテクチャに起因する制限から古典プログラムに比べてプログラムを記述するのが難しく，言語レベルでのサポートが必須である．本研究では，量子ラムダ計算を対象に，coupling graph と呼ばれる量子コンピュータのアーキテクチャ制約を満たすかどうかを検査するための型システムや，与えられたプログラムに対しそのプログラムが実行できるための coupling graph 制約を推論する型推論アルゴリズムなどを研究している．
プログラムを，人から計算機へアルゴリズムを伝えるという手段としてだけではなく，人から人へと計算システムに関する考えを伝える・共有するためのメディアであると考えると，それを記述するためのプログラミング言語も，計算機にとってわかりやすい機械語ではなく，人間にとっても意味がわかりやすいものでなくてはならない．抽象化機構とは，(計算機の)細部を隠すた めのプログラミング言語に備わった機能であり，例えば「手続き」は最も基本的な抽象化機構である．
我々は，人間にとってよりわかりやすいプログラムが書ければ，自然とプログラムの誤りも少なくなるだろう，という考えに基き，アプリケーション分野に応じた適切な抽象化機構の開発とその理論研究を行っている．
プログラミング言語のほとんどは，コンパイル時に型検査を行いエラーを検出する静的型付け言語と，エラーの検出は実行時に行う動的型付け言語に分類される．前者は，エラー検出が早い段階でできる安全性というメリットがある反面，プログラム記述の柔軟性を損なう場合がある．後者はその逆で，柔軟でプロトタイピングなどに向いているが，デバグが大変になりがちである．
このテーマでは，動的型付けされるプログラムから，静的型付けされるプログラムへの漸進的な移行や、両者の共存を可能にするための枠組み---漸進的型付けの理論---を研究している．
多段階プログラミングとは，プログラムをデータとして扱うことで，プログラムを生成するようなプログラムを組むことを指している．多段階プログラミングをサポートする言語機構としてはCやLispのマクロ機能，C++のテンプレートなどがあるが，いずれも生成されたプログラムが本当に安全なプログラムかを事前に検査することが難しい．我々は多段階プログラミングをより安全に行うための適切な言語の設計を，様相論理に基づく型理論を使って行うとともに，そういった言語の実装理論を研究している．
計算効果とは，典型的には入出力や例外処理といった「式の値を計算する際に発生するもろもろ」を指す用語である．計算効果はうまく使うとプログラムを簡潔に書ける一方で，濫用するとプログラムの動きを追うのが難しくなるため，型システムなどを使ってうまくプログラムを制限することが大切である．現在，計算効果を扱うための一般的な理論である代数的効果(algebraic effects)に対する型システムや，計算効果の仕様からその実装を自動導出する技法などを研究している．
実世界のシステムはソフトウェアのみによるものとは限らない．例えば自動車や航空機，ロボットなどの物理情報システムにおいては，システムを制御するソフトウェアの動作に加えて力学・電気系の連続量で記述される動作も重要である．物理情報システムにおいては，特に外界の挙動を事前に完全に予見することが困難であるという点に大きな困難がある．また，近年幅広く活用されている深層学習を用いたAIシステムにおいても，例えば学習されたパラメタなどを人間が理解することが困難であるという点に，従来のソフトウェアと比べて新たな課題がある．
我々は上記のような，通常のプログラムのみからならないシステムに対する，検証・解析手法の研究も行っている．特にシステム全体の完全な挙動の理解が困難である，という点に着目し，システムの内部構造の知識を前提としない技術に主に取り組んでいる．
この分野では例えば以下のような研究テーマに取り組んでいる．
実行時検証とは，システムの実行によって得られるログに対して，論理式やオートマトンなどによって与えられた形式仕様が成立しているかどうかを検査する手法である．実行時検証には 1) システムの内部構造などが不明なブラックボックスシステムに対しても適用可能である， 2) システムの安全性を網羅的に検証・証明する手法と比べて，より複雑なシステムを扱うことができる，などの利点がある．我々は実行時検証手法の高速化や，成立・不成立の判定のみではなく，「安全度合い」などより量的な判定への拡張などについて取り組んでいる．
モデル検査などの形式検証手法を用いることで，システムの安全性を網羅的に証明することができる．一方で，これらの手法を用いるにはシステムの挙動を形式的に記述する必要があり，この点がしばしば実用上の難点となる．我々はシステムの振る舞いをオートマトンなどを用いて近似的に記述した数理モデルを自動的に学習する手法や，近似数理モデルの学習手法と形式検証手法とを組み合わせることによる，自動テスト手法などについて取り組んでいる．