Development of Verification Techniques for Equivalence of Programs via Rewriting Induction

2022 Fiscal Year Final Research Report

• Project/Area Number: 18K11160
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60010:Theory of informatics-related
• Research Institution: Nagoya University
• Principal Investigator: Nishida Naoki 名古屋大学, 情報学研究科, 准教授 (00397449)
• Project Period (FY): 2018-04-01 – 2023-03-31
• Keywords: プログラム変換 / 制約付き書換え / プログラム検証 / 書換え帰納法 / 等価性 / 実行時エラー検証 / 全パス到達可能性 / 定理自動証明

Outline of Final Research Achievements

In this research project, we established a framework for verification of pointer-less imperative programs, especially C programs and LLVM intermediate representations: We first transform a program into an equivalent logically constrained term rewrite system, and then verify the rewrite system by means of rewriting induction or a proof system for all-path reachability. Then, we implemented a verification tool based on the framework. In the framework, equivalence of programs is reduced to inductive theorems, and is verified by rewriting induction. Non-occurrence of a specified runtime error is reduced to an all-path reachability problem, and is verified by a proof system based on co-induction. In addition, to compare a proof system based on rewriting induction with a cyclic proof system, for a sequent w.r.t. inductive definitions satisfying a certain condition, we showed transformations between a cyclic proof and a rewriting-induction proof for validity of the sequent.

Free Research Field

書換え理論

Academic Significance and Societal Importance of the Research Achievements

本研究では，書換え理論を実用プログラムに応用することをめざし，車載組込みシステムの検証に提案手法を応用することを試みた．この応用はこれまでにない試みであり，本研究の成果は書換え理論，特に制約付き書換えの実用性・有用性を示したと言える．さらに，これまでに研究されてきた多くの書換え理論の研究成果が提案手法を通じて応用できる可能性も示した．その観点から学術的意義だけでなく，社会的意義がある研究課題であることも示したと言える．
一方，全パス到達可能性を実行時エラーの非発生の証明に応用することも新しい試みであり，その有用性・実用性の観点から今後，さらに研究する価値がある課題であることを示した．