最近の研究テーマ

• プログラム検証

  ほとんどのシステムがコンピュータで制御されている今日、コンピュータソフトウェアの信頼性はシステムの 信頼性に直結します。我々は、プログラミング言語の型システムの概念を発展させ、モデル検査技法やオートマトン理論などと 組み合わせることにより、プログラムの様々な性質を検証するための理論を構築し、それに基づいて自動検証ツールを作成しています。 具体的には以下のようなテーマで研究を行っています．

  • 高階モデル検査とそのプログラム検証への応用
  • 並行プログラムのデッドロックやライブロックの解析

    型推論の考え方を拡張して並行プログラムの解析を行えます。 詳しくはこちら

  • ファイルやメモリなどの計算資源の利用法解析（例えばmallocされたメモリがいずれfreeされるかなど）
  • 依存型を用いた関数型言語の詳細使用の検証（例えばソーティング関数が本当にソートされたリストを返すか）

• ソフトウェアセキュリティ

  暗号プロトコルの自動検証、プログラムによる機密情報の漏洩の検証などの研究を行っています。 プロトコル検証器のデモはこちら

• データ圧縮

  木構造データなどを、それを生成するプログラムの形に圧縮し、データに対する変換やクエリ操作を圧縮したまま行うという手法について 研究しています。高階モデル検査の研究から派生した研究トピックですが、理論的には最適な圧縮を実現可能であること、 圧縮したままデータの変換やクエリ操作を行える、というのが既存のデータ圧縮と異なります。

• 型理論に基づくプログラム変換

  型理論を用いてプログラマが記述したプログラムをより効率のよいプログラムに変換する手法を研究しています。