高階不動点論理に基づくプログラム検証

2020 年度 審査結果の所見

• 研究課題/領域番号: 20H00577
• 研究種目: 基盤研究(A)
• 配分区分: 補助金
• 応募区分: 一般
• 審査区分: 中区分60:情報科学、情報工学およびその関連分野
• 研究機関: 東京大学
• 研究代表者: 小林 直樹 東京大学, 大学院情報理工学系研究科, 教授 (00262155)
• 研究分担者: 佐藤 亮介 九州大学, システム情報科学研究院, 助教 (10804677) ; 五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456) ; 海野 広志 筑波大学, システム情報系, 准教授 (80569575)
• 研究期間 (年度): 2020-04-01 – 2021-03-31

審査結果の所見の概要

本研究は、プログラムの検証技術として使われるモデル検証を拡張した高階モデル検証に基づくプログラム自動検証手法を実用レベルに引き上げる研究である。特に「高階不動点論理」による検証の理論を発展させ、実際に全自動検証器を構築し、さらにコンパイラや仮想通貨などのソフトウェアの検証で有効性を評価する。
プログラミングを伴う各種システムの高度化・複雑化が進む現在、プログラム検証の進化も期待される状況にあり、その中に於いて、高階不動点論理の可能性を探究するというテーマは、国内外の研究動向を踏まえつつも独創的で、学術的問いとして明確かつ重要である。理論面では特に高階モデル検査に関する未解決問題に取り組み、さらに確率や時間の概念を入れて拡張した高階モデル検査に関する研究により、本分野の発展が期待できる。