2018 Fiscal Year Annual Research Report
Refinement and Extension of Higher-Order Model Checking
| Project/Area Number |
15H05706
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
小林 直樹 東京大学, 大学院情報理工学系研究科, 教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
篠原 歩 東北大学, 情報科学研究科, 教授 (00226151)
佐藤 亮介 九州大学, システム情報科学研究院, 助教 (10804677)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| Project Period (FY) |
2015-05-29 – 2020-03-31
|
| Keywords | 高階モデル検査 / プログラム検証 / データ圧縮 / 高階文法 / 高階論理 |
|---|
| Outline of Annual Research Achievements |
本課題では、高階モデル検査の（１）理論的基盤の強化とそれに基づく高階モデル検査アルゴリズムの改良、（２）プログラム検証への応用、（３）高階モデル検査の拡張、（４）データ圧縮への応用、の４つを柱に研究を進めている。以下、それぞれの項目について、2018年度（およびその繰越として遂行した2019年度の一部の結果）について述べる。
（１）理論的基盤の強化：高階モデル検査の平均時計算量の分析の前準備として、単純型付きラムダ項の簡約列の長さについて、前年度までに得られた結果をさらに改良し、国際誌LMCSの論文にまとめた。また、高階モデル検査の対象である高階文法HORSに確率を加えて拡張したPHORSを考え、その停止性(almost sure termination)問題の決定不能性を証明した。
（２）プログラム検証への応用：高階モデル検査に基づくプログラム検証器MoCHiを改良するため、抽象化改良のフェーズに詳細型推論の手法を導入し、検証器の性能が向上することを確認した。並行して、CHCに基づく詳細型推論手法の改良のため、機械学習手法の導入を行った。
（３）拡張高階モデル検査：２種類の高階モデル検査の一つであるHFLモデル検査に整数を加えて拡張したHFLzモデル検査問題について前年度に引き続き研究を進め、プログラム検証問題からHFLzモデル検査問題への帰着手法を一般化し、より広範囲のプログラム検証問題を統一的にHFLzモデル検査に帰着できるようにした。また、HFLzモデル検査問題を定理証明支援器を用いて半自動で解くためのライブラリを開発した。これによって全自動検証が難しいプログラムの検証を、半自動で行えるようになった
（４）データ圧縮への応用：高階圧縮の知識発見への応用の試みの一環として、前年度に引き続き確率文脈自由文法を用いて圧縮する手法についての研究を進め、その有効性の評価を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
理論計算機科学分野のトップジャーナルの一つLMCS、理論計算機科学やプログラミング言語分野のトップレベル国際会議であるLICS, TACASなどに論文が採択されている。また、当初想定していなかったHFLz, PHORSなどの高階モデル検査の拡張に関する新しい重要な結果が得られている。
|
| Strategy for Future Research Activity |
2種類の高階モデル検査(HORSモデル検査, HFLモデル検査)については、昨年度に引き続き、より将来性のあるHFLモデル検査に基づく方式に軸足を移していく。データ圧縮については確率文法を用いた圧縮という新しい方式の有効性の検証がまだ十分でなく、引き続き改良を続けていく。
|
