Temporal and Relational Verification of High-Level Programs

2019 Fiscal Year Final Research Report

• Project/Area Number: 16H05856
• Research Category: Grant-in-Aid for Young Scientists (A)
• Allocation Type: Single-year Grants
• Research Field: Software
• Research Institution: University of Tsukuba
• Principal Investigator: Unno Hiroshi 筑波大学, システム情報系, 准教授 (80569575)
• Project Period (FY): 2016-04-01 – 2020-03-31
• Keywords: プログラム検証 / プログラミング言語 / 関係的仕様 / 時相的仕様 / 依存リファインメント型 / ホーン節制約解消 / 不動点論理 / 帰納的定理証明

Outline of Final Research Achievements

In this research, we have extended verification methods and tools based on refinement types and constrained Horn clauses to enable relational and temporal verification of high-level programs. For relational verification, we have proposed Horn constraint solving methods based on (co-)inductive theorem proving. We have also presented methods for solving first-order fixpoint logic constraints to enable temporal verification.

Free Research Field

プログラム検証

Academic Significance and Societal Importance of the Research Achievements

本研究で提案した高レベルプログラムの時相的・関係的検証のためのリファインメント型システム、不動点論理、動的論理といった検証理論・手法は、既存手法が扱えなかった高階関数や代数データ型といった発展的な言語機能を扱うことを可能とした。また、本研究では、提案した検証理論に基づき、高階関数型言語 OCaml のための検証ツール RCaml、不動点論理制約解消ツール MuVal、述語制約解消ツール PCSat の開発も行っており、今後これらのツールを実際のソフトウェア開発現場で実用可能なレベルまで発展させれば、ソフトウェアの信頼性向上に大きく貢献することが期待される。