Higher-Order Model Checking and its Applications

2015 Fiscal Year Final Research Report

• Project/Area Number: 23220001
• Research Category: Grant-in-Aid for Scientific Research (S)
• Allocation Type: Single-year Grants
• Research Field: Fundamental theory of informatics
• Research Institution: The University of Tokyo (2012-2015); Tohoku University (2011)
• Principal Investigator: Kobayashi Naoki 東京大学, 情報理工学(系)研究科, 教授 (00262155)
• Co-Investigator(Kenkyū-buntansha): SHINOHARA Ayumi 東北大学, 大学院情報科学研究科, 教授 (00226151) ; IGARASHI Atsushi 京都大学, 大学院情報学研究科, 教授 (40323456) ; UNNO Hiroshi 筑波大学, 大学院システム情報工学研究科, 助教 (80569575)
• Co-Investigator(Renkei-kenkyūsha): TERAUCHI Tachio 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70447150) ; SUMII Eijiro 東北大学, 大学院情報科学研究科, 教授 (00333550) ; MATSUDA Kazutaka 東北大学, 大学院情報科学研究科, 准教授 (10583627)
• Project Period (FY): 2011-05-31 – 2016-03-31
• Keywords: 高階モデル検査 / プログラム検証 / データ圧縮 / 高階文法 / 型システム

Outline of Final Research Achievements

The main topic of this research project was higher-order model checking, which is an extension of model checking, a representative method for system verification. In 2009, Kobayashi, the leader of this project, has developed the first practical algorithm for higher-order model checking, and also shown that higher-order model checking is useful for program verification. This research project has been launched to extend his results. The major results include: the development of much faster higher-order model checkers, implementation of fully-automated tools for program verification, and applications to data compression (where data are compressed in the form of functional programs that generate them, and compressed data are manipulated without decompression).

Free Research Field

プログラミング言語