| （理論面の）対象 | 計算モデルの持つ性質を形式的に定式化し数学的に証明すること. |
| （理論面の）目標 | 新たな計算モデルの提案とその実応用に役立つ形式体系の構築. |
| ここまでの成果/重要な発見 | さまざまな形式証明支援系の開発と証明ライブラリの蓄積.航空管制・鉄道運行等に関わるソフトウェア検証例. |
| これからの目標/現在取り組んでいる目標 | 社会で利用されているシステムのソフトウェア検証に応用可能な数学理論の形式検証ライブラリの開発と応用. |
| 応用上の成果/目標 | 安心・安全な情報・制御システムの構築と安全性の保証・証明. |
| さらなる発展の可能性・方向性 | 世界デジタル数学ライブラリ(World Digital Mathematics Library)の作成, 証明とプログラムの統一. |
(1) グラフ変換とグラフアルゴリズム，カテゴリー論のソフトウェア科学への応用 分散並列処理の可能性や新しい計算のパラダイムを模索してグラフ変換を利用したグラフ・アルゴリズムについて考える．特に，ネットワーク信頼性などの応用分野を意識し，有効なグラフ不変量の発見とその計算アルゴリズム開発に関する研究を行う．カテゴリー論についてプログラム理論，オートマトン理論，論理プログラミング，概念構成などのソフトウェア科学への応用の観点から研究指導を行う．(2) 計算機ネットワーク 計算機ネットワークを利用した情報システム，特に，暗号系を利用したシステム保護について，数学理論を利用した背景を含めて広く教育研究指導を行う．
| キーワード | ソフトウェア科学，グラフ変換理論，計算理論 |
|---|---|
| 部門 | 応用理論研究部門，数理計算インテリジェント社会実装推進部門 (兼任)，先進暗号数理デザイン室 (兼任) |
| リンク |