2018 Fiscal Year Annual Research Report
Temporal and Relational Verification of High-Level Programs
| Project/Area Number |
16H05856
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| Project Period (FY) |
2016-04-01 – 2020-03-31
|
| Keywords | 時相的仕様 / 関係的仕様 / 不動点論理 / 述語充足可能性判定 / 循環証明 / プログラム検証 |
|---|
| Outline of Annual Research Achievements |
本研究では、研究代表者がこれまでに研究・開発を行ってきた高レベル言語のための検証理論であるリファインメント型システムおよびホーン節制約解消法、関数型言語 OCaml のための全自動・高精度検証ツールである RCaml を発展させ、実用上重要であるにも関わらず既存手法では十分に扱えなかった言語機能（再帰データ構造・参照セル・オブジェクト・モジュール機構・例外処理機構・マルチスレッド機構）および仕様（時相的仕様・関係的仕様）の全自動・高精度検証法の確立を目指している。前年度までの成果である、依存リファインメント型・エフェクトシステムによる依存時相仕様検証問題から不動点論理式の妥当性判定問題への帰着法と妥当性判定のための演繹体系だけでは、全自動で高レベルプログラムの検証を行うことができなかった。そこで、本年度は依存時相仕様および関係的仕様の自動検証の実現を目指して研究を行い、以下の成果を得た。(1) 不動点論理の妥当性判定問題の自動解消法を提案した。提案手法は妥当性判定問題を、ホーン節制約解消問題を一般化した述語制約解消問題に帰着した上で、反例駆動帰納的合成法と決定木学習、テンプレートに基づく解探索法を組み合わせて解くものである。(2) 述語制約解消問題を解くための別の手法として、機械学習分野で研究されてきた因子グラフおよびマルコフ確率場のための確率伝搬法とシステム検証分野で研究されてきた反例駆動帰納的合成法、述語抽象、SATソルバを組み合わせたものを提案した。(3) 不動点論理式の妥当性判定を関係的仕様検証に応用できるようにするため、一階不動点論理の循環証明体系を提案し、前年度までの成果である不動点論理の妥当性判定のための演繹体系との関係を調査した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究実績の概要で述べたとおり、ホーン節制約解消問題を一般化した述語充足可能性判定問題の解消法、不動点論理の妥当性判定の述語充足可能性判定への帰着法、不動点論理の妥当性判定のための循環証明体系といった先駆的な成果を得ている。これらの成果の一部は、ホーン節制約解消に関する国際ワークショップであるHCVS'18の招待講演で発表した。また、HCVS'19併設のCHC競技会に提案手法を実装したツールであるPCSatを提出し、類似ソルバとの比較評価を行うなど、理論面だけでなく実装・評価においても大きな進展があった。
|
| Strategy for Future Research Activity |
今後も計画通り研究を推進する。2019年度には、これまでに得られた依存リファインメント型・エフェクトシステムに関する研究成果に基づき、OCaml言語用検証ツールRCamlを拡張することによって、高階・再帰データ構造、参照セル、オブジェクト、モジュール機構、例外処理機構、マルチスレッド機構といった高度な言語機能を扱うOCamlやJavaで記述された高レベルプログラムを対象とし、その依存時相仕様検証問題を不動点論理の妥当性判定問題に帰着するツールを完成させる。それと今年度までの成果である不動点論理の妥当性判定のためのソルバを組み合わせることによって、高レベルプログラムの時相的仕様検証および関係的仕様検証、それらを包含する仕様クラスであるHyperpropertiesの全自動検証が実現する。さらに、検証法の評価のために、情報セキュリティ（機密性・完全性・可用性）への応用を行う。
|
