| Co-Investigator(Kenkyū-buntansha) |
篠原 歩 東北大学, 情報科学研究科, 教授 (00226151)
佐藤 亮介 九州大学, システム情報科学研究院, 助教 (10804677)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| Budget Amount *help |
¥193,960,000 (Direct Cost: ¥149,200,000、Indirect Cost: ¥44,760,000)
Fiscal Year 2019: ¥38,610,000 (Direct Cost: ¥29,700,000、Indirect Cost: ¥8,910,000)
Fiscal Year 2018: ¥37,960,000 (Direct Cost: ¥29,200,000、Indirect Cost: ¥8,760,000)
Fiscal Year 2017: ¥39,780,000 (Direct Cost: ¥30,600,000、Indirect Cost: ¥9,180,000)
Fiscal Year 2016: ¥41,600,000 (Direct Cost: ¥32,000,000、Indirect Cost: ¥9,600,000)
Fiscal Year 2015: ¥36,010,000 (Direct Cost: ¥27,700,000、Indirect Cost: ¥8,310,000)
|
|---|
| 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.
|
