Higher-order program verification via HFL model checking

DOI10.1007/978-3-319-89884-1_25zbMATH Open1418.68127arXiv1710.08614OpenAlexW2963426974MaRDI QIDQ2324003FDOQ2324003

Takeshi Tsukada, Keiichi Watanabe, Naoki Kobayashi

Publication date: 13 September 2019

Abstract: There are two kinds of higher-order extensions of model checking: HORS model checking and HFL model checking. Whilst the former has been applied to automated verification of higher-order functional programs, applications of the latter have not been well studied. In the present paper, we show that various verification problems for functional programs, including may/must-reachability, trace properties, and linear-time temporal properties (and their negations), can be naturally reduced to (extended) HFL model checking. The reductions yield a sound and complete logical characterization of those program properties. Compared with the previous approaches based on HORS model checking, our approach provides a more uniform, streamlined method for higher-order program verification.

Full work available at URL: https://arxiv.org/abs/1710.08614

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (9)

• On higher-order reachability games vs may reachability
• Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking
• Fold/Unfold Transformations for Fixpoint Logic
• Title not available (Why is that?)
• An overview of the HFL model checking project
• Reducing higher-order recursion scheme equivalence to coinductive higher-order constrained Horn clauses
• Crowfoot: A Verifier for Higher-Order Store Programs
• A type-based HFL model checking algorithm
• Temporal verification of programs via first-order fixpoint logic

Recommendations

• Model Checking Higher-Order Programs 👍 👎
• Modular Verification of Higher-Order Functional Programs 👍 👎
• Higher order generalization and its application in program verification 👍 👎
• Exact Flow Analysis by Higher-Order Model Checking 👍 👎
• Higher-Order Model Checking: An Overview 👍 👎
• Higher-Order Model Checking in Direct Style 👍 👎
• Title not available (Why is that?) 👍 👎

This page was built for publication: Higher-order program verification via HFL model checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2324003)