教員

個人ページ

https://www.riec.tohoku.ac.jp/~unno/

研究活動

現代社会において、人々は日常的にスマートフォンやコンピュータを私生活や仕事に用いており、普段意識されない交通・金融・医療・エネルギーといった社会基盤もコンピュータにより制御されている。したがって、コンピュータを動かすプログラムであるソフトウェアの信頼性を確保し、効率性を向上させることは、社会の安定と円滑な機能の維持にとって重要な課題となっている。本研究室では、形式論理やプログラム理論といった基礎理論に基づいた高信頼・高効率ソフトウェア構成技術の研究を行っている。

ソフトウェア構成研究分野｜海野教授

研究テーマ

• プログラム検証およびプログラム合成
• プログラミング言語と型システム
• 制約解消・最適化
• 自動定理証明

本分野では、与えられたプログラムがその仕様を満たすことを数学的に厳密に保証するための技術であるプログラム検証や、仕様からそれを満たすプログラムを生成するための技術であるプログラム合成の研究・開発を進めている。具体的には、関数型プログラミング言語 OCaml に検証・合成ツールを統合することによって、高信頼・高効率プログラムの開発を促進することを目指した RCaml や、多様な検証・合成問題を述語制約や不動点論理式として表現して解くことができるソルバである PCSat や MuVal, MuCyc の研究・開発を行っている。
また、これらのツールの基礎となるプログラム理論や型理論、制約解消・最適化の理論、不動点論理とその演繹体系についても研究を行っている。特に最近のソフトウェアは、並行・並列・分散的な動作や機械学習モデルへの依存、暗号プロトコルや確率プログラム、乱択アルゴリズムにおけるランダム性の本質的な利用などにより、ますます複雑化している。そのため、既存の理論だけでは対処しきれない複雑性に対処するための理論構築にも力を注いでいる。