Refinement and Extension of Higher-Order Model Checking

2020 Fiscal Year Final Research Report

• Project/Area Number: 15H05706
• Research Category: Grant-in-Aid for Scientific Research (S)
• Allocation Type: Single-year Grants
• Research Field: Theory of informatics
• Research Institution: The University of Tokyo
• Principal Investigator: Kobayashi Naoki 東京大学, 大学院情報理工学系研究科, 教授 (00262155)
• Co-Investigator(Kenkyū-buntansha): 篠原 歩 東北大学, 情報科学研究科, 教授 (00226151) ; 佐藤 亮介 九州大学, システム情報科学研究院, 助教 (10804677) ; 五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456) ; 海野 広志 筑波大学, システム情報系, 准教授 (80569575)
• Project Period (FY): 2015-05-29 – 2020-03-31
• Keywords: 高階モデル検査 / プログラム検証 / データ圧縮 / 型システム / 関数型プログラム / 高階不動点論理

Outline of Final Research Achievements

This research aimed to advance the theory of higher-order　model checking and its applications. We have obtained good theoretical results, such as a pumping lemma for higher-order languages and the surprising connection between two kinds of higher-order model checking. We have also made progress in the applications of higher-order model checking, such as the big improvement in the efficiency of higher-order model checkers and program verification tools and in the class of program properties that can be verified, and a new technique for higher-order data compression using arithmetic coding.

Free Research Field

プログラミング言語、プログラム検証

Academic Significance and Societal Importance of the Research Achievements

上述の成果は、代表者の専門であるプログラム検証などプログラミング言語分野・ソフトウェアの基礎理論のみならず、反復補題に関する40年以上ぶりの進展など、形式言語理論、計算量理論、データ圧縮など周辺の様々な学問分野に新たな知見をもたらすものであり、学術的意義が大きい。また、プログラムの自動検証技術を大きく進展させ、社会基盤を支えるコンピュータシステムの安全性向上に寄与するという社会的意義も大きい。