• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2015 Fiscal Year Final Research Report

Higher-Order Model Checking and its Applications

Research Project

  • PDF
Project/Area Number 23220001
Research Category

Grant-in-Aid for Scientific Research (S)

Allocation TypeSingle-year Grants
Research Field Fundamental theory of informatics
Research InstitutionThe 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

プログラミング言語

URL: 

Published: 2017-05-10  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi