| 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
|
| Project Status |
Completed (Fiscal Year 2015)
|
| Budget Amount *help |
¥137,540,000 (Direct Cost: ¥105,800,000、Indirect Cost: ¥31,740,000)
Fiscal Year 2015: ¥28,990,000 (Direct Cost: ¥22,300,000、Indirect Cost: ¥6,690,000)
Fiscal Year 2014: ¥29,120,000 (Direct Cost: ¥22,400,000、Indirect Cost: ¥6,720,000)
Fiscal Year 2013: ¥28,080,000 (Direct Cost: ¥21,600,000、Indirect Cost: ¥6,480,000)
Fiscal Year 2012: ¥28,730,000 (Direct Cost: ¥22,100,000、Indirect Cost: ¥6,630,000)
Fiscal Year 2011: ¥22,620,000 (Direct Cost: ¥17,400,000、Indirect Cost: ¥5,220,000)
|
|---|
| 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).
|
| Assessment Rating |
Verification Result (Rating)
A
|
Assessment Rating |
Result (Rating)
A: Progress in the research is steadily towards the initial goal. Expected research results are expected.
|
