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

定理証明支援ツールを使って、安全なソフトウェアを作る

教員

教授：アフェルトレナルド
准教授：川本裕輔

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

数学的な応用に関心を持ち、物事を形式化したり自動的に推論したりすることに興味を持っていることが重要です。また、記号論理と関数型プログラミング言語についての基礎知識が必要になります。

研究室の指導方針

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

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

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

形式論理の応用・実装を通じて、高度な論理的能力と抽象的思考力を身に付けることができます。これらの能力は、AIに仕事を奪われると言われる時代において重要なアドバンテージとなりますが、情報科学の応用分野の研究教育だけでは十分に習得できない能力です。このほかにも、テクニカルライティングの指導や国際共同研究を通じて、技術英語を論理的に読み書きする能力を習得できます。

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

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

研究内容

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

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