物理的・確率的システムの検証を支える形式的基盤の構築

2022 Fiscal Year Comments on the Screening Results

• Project/Area Number: 22H00520
• Research Category: Grant-in-Aid for Scientific Research (A)
• Allocation Type: Single-year Grants
• Section: 一般
• Review Section: Medium-sized Section 60:Information science, computer engineering, and related fields
• Research Institution: National Institute of Advanced Industrial Science and Technology
• Principal Investigator: Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 上級主任研究員 (40415641)
• Co-Investigator(Kenkyū-buntansha): 才川 隆文 名古屋大学, 多元数理科学研究科, 研究員 (00897100) ; 勝股 審也 京都産業大学, 理学部, 教授 (30378963) ; 中野 圭介 東北大学, 電気通信研究所, 教授 (30505839) ; 溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783) ; J Garrigue 名古屋大学, 多元数理科学研究科, 教授 (80273530)
• Project Period (FY): 2022-04-01 – 2026-03-31

Summary of the Research Project

外界との相互作用を行うプログラムの検証技術の確立を目指して、物理的対象としての外界を扱うための機械検証可能な数学的基盤（実解析、確率論、幾何学等）を構築することを目指している。またそれらのプログラムの検証を可能にするためのプログラム意味論の形式化を圏論を主軸として推進し、等式推論を主軸としたプログラムの形式検証基盤の構築を目指している。

Scientific Significance and Expected Research Achievements

連続量や確率や外界との相互作用を扱うプログラムのための形式化はこれまで多くの理論研究があったが、本研究は定理証明支援系という汎用で統一的な枠組の上で、上記の特徴をもつプログラムの性質を扱うための幅広い数学の体系化とライブラリ化を多項目にわたって推進する点に意義がある。情報学の基礎研究と位置づけられるが、強固な数学的基盤に基づく再利用性の高い成果物が期待できる。