2022 Fiscal Year Annual Research Report
Development of Verification Techniques for Equivalence of Programs via Rewriting Induction
| Project/Area Number |
18K11160
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
西田 直樹 名古屋大学, 情報学研究科, 准教授 (00397449)
|
|---|
| Project Period (FY) |
2018-04-01 – 2023-03-31
|
| Keywords | プログラム検証 / 制約付き書換え / プログラム変換 / 計算モデル / 帰納法 / 定理自動証明 / 実行時エラー検証 / 到達可能性 |
|---|
| Outline of Annual Research Achievements |
研究計画当初における最終年度の課題である（A1）書換え帰納法の推論規則の適用戦略の開発，（A2）補題等式の自動生成法の開発に取り組んだ．さらに，3，4年目に設定した課題である（D）LCTRSによる並行プログラムのモデル化，（E）ビットベクトルをデータとして扱うLCTRSの停止性証明法の開発，（F）等価性ではなく全パス到達可能性（all-path reachability）に帰着させて検証する枠組みの開発に取り組み，本研究で開発している書換え帰納法の対話的証明ツールに全パス到達可能性問題の自動証明機能を実装した．
（A1）と（A2）については書換え帰納法の推論規則に基づいて実現した全パス到達可能性問題の自動証明機能の実現のために，幅優先探索に基づく推論規則の適用戦略を開発し，実装した．証明に失敗する例に対して，検証したいLCTRSが表現するシステムの初期状態を一般化する補題生成の有効性を実験により確認した．
（D）については非同期整数状態遷移システム，居眠り床屋問題，並行バグを含む例をLCTRSに変換し，競合状態・スタベーションが発生しないことを検証する実験を実施した．
（E）については3年目に開発した停止性証明法の証明力強化と自動化に向けて，単一自己ループに対する証明の改良，ビットベクトル上の多項式解釈の提案とそれを利用した証明法を開発した．
（F）についてはスタベーションが発生しないことを全パス到達可能性問題に帰着して証明するためのLCTRSの変換方法を提案した．さらに，反証方法，公平でないパスを除外した証明法を提案し，実装した．そして，（D）におけるベンチマークに対して実装の実行時間を評価し，提案手法のスケーラビリティについて考察した．
|
