2021 Fiscal Year Research-status 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 |
研究計画当初における4年目の課題である(A1)書換え帰納法の推論規則の適用戦略の開発，(A2)補題等式の自動生成法の開発，(B)様々な書換えシステムへの拡張，さらに，それまでの進捗情況を踏まえて3年目から設定した(D)LCTRSによる並行プログラムのモデル化，(E)ビットベクトルをデータとして扱うLCTRSの停止性証明法の開発に取り組んだ．
(A1)と(A2)については前年度に開発した補題生成法をまとめ，成果発表を行なった．そして自動証明の中での補題生成法の効果的な使用を目指して推論規則の適用戦略について検討した．
(B)については3年目から継続して，停止性を持つ項書換えシステムを対象にして循環証明システムと書換え帰納法を比較する課題に取り組み，限定したクラスの証明に関しては2つの証明法の証明能力が等しいことを証明した．さらに，提案手法が対象とするプログラミング言語を拡大することを目的に，LLVM中間表現を対象とするように拡張を行なった．従来の対象としていたC言語プログラムをコンパイルして得られるLLVM中間表現（主にポインタを扱わないもの）に対する変換を提案した．
(D)についてはバイナリセマフォによる排他制御を含むプログラムからLCTRSへの変換（3年目に提案）を計数セマフォに提案した．さらに，排他制御に成功していることをこれまで開発してきた等価性検証の枠組みで行えるかどうかについて検討し，等価性ではなく全パス到達可能性（all-path reachability）に帰着させて検証する枠組みを提案した．全パス到達可能性の証明システムは書換え帰納法の推論規則の使用を限定して実現できることを示し，開発している検証ツールの証明機能を制限することで全パス到達可能性を証明する機能を追加実装した．
(E)については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
当初に計画していた4年目までの課題については概ね達成できた．特に，循環証明システムと書換え帰納法の比較については提案手法の証明力を理論的に示す課題であり，対象が限定的ではあるが，昨今プログラム検証手法の1つとして注目されている循環証明システムと証明能力が等しいことを示せた成果は当初の想定よりも早い段階で得た成果である．
本研究の目的の一つは車載組込みシステムの検証などの応用が可能な定理自動証明ツールの開発である．4年目に排他制御に成功していることを等価性に帰着することを検討する過程で，提案手法を当初の目的である応用という点で，書換え帰納法と類似した推論規則により証明できる全パス到達可能性への帰着が適していると判断した．そして，これまでの開発ツールの証明機能を制限するだけで全パス到達可能性を証明する機能を実装できた点は，当初に予定していなかった大きな成果である．
以上のことから本研究の進行状況は概ね順調であると言える．
|
| Strategy for Future Research Activity |
4年目までの成果から，今後はプログラムをより忠実に表現できるモデルとしてビットベクトルをデータとして扱うLCTRSを採用し，等価性だけでなく実行時エラーが発生しないことなども検証できる定理自動証明ツールの開発を目指す．
ビットベクトルを扱うLCTRSツールの開発は急務である．そこで4年目に引き続き，ビットベクトルを扱うLCTRSの停止性証明機能の実装に取り組む．開発ツールは制約の充足可能性判定のためにSMTソルバを呼び出すが，現在の実装はビットベクトル制約の扱いが脆弱であり，SMTソルバの証明力を十分に利用できていない．よって，開発ツールのデータ構造を見直し，ツールを改良する．
4年目に導入した全パス到達可能性の証明機能についてもさらなる改良に取り組む．特に，指定した実行時エラー（排他制御の成功やリソーススタベーション）からLCTRSへの変換の定式化に取り組む．また，実装した全パス到達可能性の証明機能は書換え帰納法の機能を制限して実現しているため，効率が悪い部分がある．そこで，開発ツールのデータ構造の見直しに合わせて，必要に応じて全パス到達可能性の証明に特化した機能を実装する．一方，循環性を利用した証明ステップについては探索空間を制限していないため，実行時間が大きい．循環性の利用のための探索空間についても検討を行い，効率の改善を図る．
開発ツールの評価および改良に向けては，引き続き，循環証明システムとの比較に取り組む．
|
| Causes of Carryover |
コロナ禍のため2020年度には成果発表の場のすべてがオンラインとなり，2021年度には成果発表での出張が増加することを見越して繰り越したが，2021年度も引き続き成果発表の場のほとんどがオンラインとなり，出張が1件（1人）しかなかったため旅費がほとんど発生しなかった．その分，オンラインでの研究打合せのための設備の購入に充てたが，2020年度から繰り越した分までを使い切るに至らなかった．2022年度に発表のための出張の回数，人員が増加することを見越して，十分な旅費を確保するために繰り越した．
当初の計画では2022年度は成果発表や研究打合せのための旅費を主な用途としていた．2021年度の成果から2022年度は予定よりも多い成果発表を予定しており，繰り越した分とは予定よりも増加する成果発表のための旅費として使用する予定である．
|
