数学に基づく問題のモデル化，仕様記述，検証，開発を支援する技術である形式手法をテーマに，正しいソフトウェアを作る方法や支援環境の構築を目指します．

形式手法による高信頼なソフトウェア開発支援

高信頼なソフトウェアをモデル化，設計，検証，開発するための形式手法（フォーマルメソッド，Formal methods）に関する研究テーマです．

プログラミング（実装／コーディング）の前の分析・設計フェーズにおいては，クラス図やシーケンス図などのUMLに代表される図的表現がよく用いられます．形式手法では，プログラミング言語とは別の形式仕様言語という種類の言語を用いてモデル化，設計を行います．

形式仕様を厳密に記述することで，プログラミング前の上流工程でコンピュータの支援のもとに，数学的に，システムの誤りを発見したり正しさを検証したりすることができます．

具体的には，代数をモデルに持つ形式仕様言語CafeOBJを対象とした研究を進めています．

書き換えシステムによる定理自動証明

等式を，コンピュータを使って自動で推論する書き換えシステム（Rewriting systems）に関する研究テーマです．

等式の集合（公理）から与えられた等式（定理）が導出可能かどうかを証明することを，等式推論といいます．等式は，左から右にも，右から左にも使えるので，コンピュータにそのまま使わせると無限に広い空間を探索する必要があります．

書き換えシステムは，公理を左から右にだけ使える書き換え規則の集合とみなして，証明したい等式の両辺の答えを求めて比較することで，定理を証明します．