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

2022 年度 審査結果の所見

• 研究課題/領域番号: 22H00520
• 研究種目: 基盤研究(A)
• 配分区分: 補助金
• 応募区分: 一般
• 審査区分: 中区分60:情報科学、情報工学およびその関連分野
• 研究機関: 国立研究開発法人産業技術総合研究所
• 研究代表者: Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 上級主任研究員 (40415641)
• 研究分担者: 才川 隆文 名古屋大学, 多元数理科学研究科, 研究員 (00897100) ; 勝股 審也 京都産業大学, 理学部, 教授 (30378963) ; 中野 圭介 東北大学, 電気通信研究所, 教授 (30505839) ; 溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783) ; J Garrigue 名古屋大学, 多元数理科学研究科, 教授 (80273530)
• 研究期間 (年度): 2022-04-01 – 2026-03-31

研究の概要

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

学術的意義、期待される成果

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