Temporal and Relational Verification of High-Level Programs

• 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
• Project Status: Completed (Fiscal Year 2019)
• Budget Amount: ¥14,560,000 (Direct Cost: ¥11,200,000、Indirect Cost: ¥3,360,000); Fiscal Year 2019: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000); Fiscal Year 2018: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000); Fiscal Year 2017: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000); Fiscal Year 2016: ¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000)
• 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.

Academic Significance and Societal Importance of the Research Achievements

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

Research Products

• [Int'l Joint Research] Stevens Institute of Technology(米国)
• [Int'l Joint Research] Verimag(France)
• [Int'l Joint Research] Yale University(米国)
• [Journal Article] Probabilistic Inference for Predicate Constraint Satisfaction (2020)
  • Author(s): Yuki Satake, Hiroshi Unno, and Hinata Yanagi
  • Journal Title: Proceedings of the annual AAAI Conference on Artificial Intelligence (AAAI 2020) Volume: 印刷中
  • Peer Reviewed / Open Access
• [Journal Article] Temporal Verification of Programs via First-Order Fixpoint Logic (2019)
  • Author(s): Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, Hiroshi Unno
  • Journal Title: In Proceedings of the 26th International Symposium (SAS 2019), Lecture Notes in Computer Science Volume: 11822 Pages: 413-436
  • DOI: 10.1007/978-3-030-32304-2_20
  • ISBN: 9783030323035, 9783030323042
  • Peer Reviewed
• [Journal Article] Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs (2018)
  • Author(s): Hiroshi Unno, Yuki Satake, and Tachio Terauchi
  • Journal Title: Proceedings of the 45th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2018), PACMPL Volume: 2 Issue: POPL Pages: 1-29
  • DOI: 10.1145/3158100
  • Peer Reviewed / Open Access
• [Journal Article] Propositional Dynamic Logic for Higher-Order Functional Programs (2018)
  • Author(s): Yuki Satake, Hiroshi Unno
  • Journal Title: Proceedings of CAV 2018, LNCS Volume: 印刷中
  • Peer Reviewed
• [Journal Article] A Fixpoint Logic and Dependent Effects for Temporal Property Verification (2018)
  • Author(s): Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
  • Journal Title: Proceedings of LICS 2018 Volume: 印刷中 Pages: 759-768
  • DOI: 10.1145/3209108.3209204
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] Automating Induction for Solving Horn Clauses (2017)
  • Author(s): Hiroshi Unno, Sho Torii, Hiroki Sakamoto
  • Journal Title: Proceedings of CAV 2017, LNCS Volume: 印刷中
  • Peer Reviewed / Acknowledgement Compliant
• [Presentation] Probabilistic Inference for Predicate Constraint Satisfaction (2020)
  • Author(s): Yuki Satake, Hiroshi Unno, and Hinata Yanagi
  • Organizer: The annual AAAI Conference on Artificial Intelligence (AAAI 2020)
  • Int'l Joint Research
• [Presentation] Temporal Verification of Programs via First-Order Fixpoint Logic (2019)
  • Author(s): NaokiKobayashi, Takeshi Nishikawa, Atsushi Igarashi, Hiroshi Unno
  • Organizer: The 26th International Static Analysis Symposium (SAS 2019)
  • Int'l Joint Research
• [Presentation] Belief Propagation for Predicate Satisfiability Checking（ポスター発表） (2019)
  • Author(s): 柳 日向, 海野 広志
  • Organizer: 第21回プログラミングおよびプログラミング言語ワークショップ
• [Presentation] Propositional Dynamic Logic for Higher-Order Functional Programs (2019)
  • Author(s): Yuki Satake, Hiroshi Unno
  • Organizer: 第21回プログラミングおよびプログラミング言語ワークショップ
• [Presentation] A Fixpoint Logic and Dependent Effects for Temporal Property Verification (2019)
  • Author(s): Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
  • Organizer: 第21回プログラミングおよびプログラミング言語ワークショップ
• [Presentation] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic (2019)
  • Author(s): Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
  • Organizer: 第21回プログラミングおよびプログラミング言語ワークショップ
• [Presentation] Horn Clauses and Beyond for Relational and Temporal Program Verification (2018)
  • Author(s): Hiroshi Unno
  • Organizer: The 5th Workshop on Horn Clauses for Verification and Synthesis (HCVS'18)
  • Int'l Joint Research / Invited
• [Presentation] 一階不動点論理の循環証明体系とプログラム検証への応用 (2018)
  • Author(s): 南條 陽史, 海野 広志
  • Organizer: 日本ソフトウェア科学会第35回大会
• [Presentation] On Cut-elimination in Cycle Proof Systems（ポスター発表） (2018)
  • Author(s): Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
  • Organizer: The 16th Asian Symposium on Programming Languages and Systems (APLAS'18)
  • Int'l Joint Research
• [Presentation] On Cut-elimination in Cycle Proof Systems (2018)
  • Author(s): Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
  • Organizer: The 4th Workshop on New Ideas and Emerging Results (NIER'18)
  • Int'l Joint Research
• [Presentation] Dependent Temporal Effects and Fixpoint Logic for Verification (2018)
  • Author(s): Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
  • Organizer: 第20回プログラミングおよびプログラミング言語ワーク ショップ（PPL2018）
• [Presentation] Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs (2018)
  • Author(s): Hiroshi Unno, Yuki Satake, Tachio Terauchi
  • Organizer: ACM Symposium on Principles of Programming Languages
  • Int'l Joint Research
• [Presentation] Propositional Dynamic Logic for Higher-Order Functional Programs (2018)
  • Author(s): Yuki Satake, Hiroshi Unno
  • Organizer: International Conference on Computer Aided Verification
  • Int'l Joint Research
• [Presentation] A Fixpoint Logic and Dependent Effects for Temporal Property Verification (2018)
  • Author(s): Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
  • Organizer: ACM/IEEE Symposium on Logic in Computer Science
  • Int'l Joint Research
• [Presentation] 関係的仕様からの関数型プログラム合成 (2017)
  • Author(s): 中尾 收, 佐竹 佑規, 海野 広志
  • Organizer: 日本ソフトウェア科学会第34回大会
• [Presentation] 余帰納法に基づく定理証明の自動化 (2017)
  • Author(s): 四宮 誠一, 海野 広志
  • Organizer: 日本ソフトウェア科学会第34回大会
• [Presentation] Temporal Logics for Higher-Order Functional Programs based on Trace Semantics（ポスター発表） (2017)
  • Author(s): Yuki Satake, Hiroshi Unno
  • Organizer: 第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）
  • Place of Presentation: 華やぎの章 慶山（山梨県笛吹市）
• [Presentation] A Horn Constraint Solver based on Inductive Theorem Proving（ポスター発表） (2017)
  • Author(s): Hiroki Sakamoto, Sho Torii, Shu Nakao, Hiroshi Unno
  • Organizer: 第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）
  • Place of Presentation: 華やぎの章 慶山（山梨県笛吹市）
• [Presentation] Temporal Dependent Contracts for Higher-Order Functions (2016)
  • Author(s): 佐竹 佑規, 海野 広志
  • Organizer: 日本ソフトウェア科学会第33回大会
  • Place of Presentation: 東北大学（宮城県仙台市）