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

2020 Fiscal Year Comments on the Screening Results

• Project/Area Number: 20H00577
• 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: The University of Tokyo
• Principal Investigator: 小林 直樹 東京大学, 大学院情報理工学系研究科, 教授 (00262155)
• Co-Investigator(Kenkyū-buntansha): 佐藤 亮介 九州大学, システム情報科学研究院, 助教 (10804677) ; 五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456) ; 海野 広志 筑波大学, システム情報系, 准教授 (80569575)
• Project Period (FY): 2020-04-01 – 2021-03-31

Outline of Opinions Expressed in the Review Results

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