2018 Fiscal Year Annual Research Report
Verification of high-level programs containing mutable higher-order recursive data structures
| Project/Area Number |
17H01720
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
寺内 多智弘 早稲田大学, 理工学術院, 教授 (70447150)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| Project Period (FY) |
2017-04-01 – 2022-03-31
|
| Keywords | プログラム検証 / ソフトウェアモデル検査 / 型システム / 自動定理証明 / 分離論理 / 循環証明 |
|---|
| Outline of Annual Research Achievements |
依存型・依存エフェクトシステムと一階述語不動点論理(first-order fixpoint logic)による高階プログラムの時相論理仕様検証に関する研究を行った。研究の成果をまとめた論文は理論計算機科学分野におけるトップ国際会議LICS 2018に採録された。また、関連して、一階述語不動点論理式の真偽性を解く自動定理証明アルゴリズムの研究および一階述語不動点論理による双模倣性の検証などのについても研究を推進し、The 5th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2018)およびThird Workshop on Mathematical Logic and its Applications (MLA 2019)にてこの研究に関する講演を行った。
また、循環証明(cyclic proof)と分離論理(separation logic)に関する研究も行った。具体的には、循環証明による分離論理の定理証明は、再帰データ構造を含む場合カット除去不可能であることを示した。この研究に関してThe 4th Workshop on New Ideas and Emerging Results in Programming Languages and Systems (NIER 2018)、日本ソフトウェア科学会 第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)およびMLA2019にて講演を行った。
加えて、サイドチャネル攻撃に対する耐タンパ性の検証など情報セキュリティに関するプログラム検証の研究を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究はおおむね順調に進展している。「研究実績の概要」で述べた通り、今年度は、特に再帰データ構造に対する破壊的代入を含むプログラムの検証に適したプログラム論理である分離論理のための自動定理証明に関する研究および高階関数を含むプログラムの検証に関する研究を行い成果を得た。来年度以降は、今年度の研究で得た知見をもとに、高階関数および破壊的代入可能な再帰データ構造を含むプログラムの検証に有効な枠組みの構築を目指す。
|
| Strategy for Future Research Activity |
今年度の研究で得られた知見をもとに研究を推進する。これまでの研究から帰納的定義を含む分離論理とリファイント型システムを融合したプログラム検証枠組みが有効と推測され、この枠組みの確立を目指す。分離論理において帰納的定義は再帰データ構造を表すために用いられるが、既存の分離論理を用いた自動プログラム検証は帰納的定義を十分に扱えず再帰データ構造の扱いは不十分である。今後は、分離論理の自動定理証明やポイントサンプリングによる不変条件推論などの技術を応用することにより、効果的な自動検証の枠組みの確立を目指す。また、リファインメント型と融合することにより高階関数の扱いおよび型による柔軟なユーザーインタフェースの提供も期待される。
また、自動・半自動プログラム検証の鍵となる自動定理証明技術についての研究も行う。具体的には、今年度に引き続き循環証明による帰納的定義を含む分離論理のための定理証明および一階述語不動点論理のための自動定理証明の研究を行う。前者は上記の通り再帰データ構造への破壊的代入を含むプログラムの検証に有効な枠組みであり、また、後者の論理は(破壊的データ構造を含むプログラムの検証には直接用いられないが)再帰関数・ループを含むプログラムの検証を直接的に表現することができる。加えて、様々な論理における量化子付き式のためのより効率よい自動証明についての研究も行う。
|
