形式検証研究室（国立研究開発法人産業技術総合研究所）

教員

研究を始めるのに必要な知識・能力など

数学的な応用に関心を持ち、物事を形式化したいという願望と熱意を持っていることが必要です。 また、形式論理とプログラミング言語理論についての基礎知識（関数型プログラミング言語、型理論など）が必要になります。

研究室の指導方針

まず、形式検証技術についての基礎知識を身につけていただきます。 その後、教員から既存技術や研究課題を紹介し、学生の関心や希望に応じて、研究テーマを相談し決定します。 学生の自発的な取り組みを重視し、定期的な研究打ち合わせを通じて議論と進捗確認を行います。 最終的に論文やソフトウェアなどの成果物を発表することを目指します。

現時点ではオンラインでの研究打ち合わせを中心に行いますが、産総研臨海副都心センター（東京都江東区）に定期的に（または長期間）来ていただくことを想定しています。

この研究室で身につく能力

ソフトウェア科学、特に形式検証技術の知識を習得できます。 研究や議論を通じて、ソフトウェア開発に有用な論理的能力や抽象的思考力を身につけることができます。 また、テクニカルライティングや研究発表などを通じて、技術英語を論理的に読み書きする能力を身につけていただきます。

産業技術総合研究所について

産業技術総合研究所（産総研）は日本最大級の公的研究機関です。 当研究室は産総研臨海副都心センターにあり、デジタルアーキテクチャ研究センター（DigiARC）に所属しています。

研究内容

形式手法（formal methods）はソフトウェアやハードウェアの正しさを数理的に厳密に検証するための技術です。 例えば、バグのないプログラム、安全な暗号プロトコル、信頼性の高いOSなどを開発するために、 様々な形式検証技術や形式検証ツールがこれまでに研究されてきました。 形式手法は安心安全なデジタル社会を築いていく上で重要な技術となっています。

当研究室では、確率的事象や物理環境などの不確実性を扱うソフトウェアシステムの仕様記述・検証のための形式手法について研究しています。 形式手法の検証対象としては、ソフトウェアの安全性、 ロボット等のサイバーフィジカルシステムの安全性、 統計ソフトウェアの正当性などのテーマに取り組んでいます。 また、その基盤技術として、数学やプログラミング言語などの形式化にも取り組んでいます。

Fig. 1 形式検証の概要

Fig. 1 形式検証の概要

定理証明支援系

定理証明支援系は、数学の証明を形式論理を用いて記述し、その正しさを厳密に確かめるためのソフトウェアです。 当研究室では、定理証明支援系Coqを利用して、数学やプログラミング言語などの形式化に取り組んでいます。

Fig. 2 Coqでの形式証明

Fig. 2 Coqでの形式証明

ソフトウェア検証

物理環境との相互作用や大規模データからの学習などによる不確実性のもとでのソフトウェアの正しさや安全性の形式化・検証のための研究に取り組んでいます。

現在の研究テーマ:

Fig. 3 SCARAロボットアーム

Fig. 3 SCARAロボットアーム

数学の形式化

ソフトウェアの厳密な検証は、数学の定理の証明に基づいています。 例えば、ロボティクスの検証では代数、 サイバーフィジカルシステムの検証では実解析、 統計ソフトウェアの検証では確率論が必要になります。 そこで、当研究室では定理証明支援系Coqを用いた数学の形式化に取り組んでいます。

現在の研究テーマ: