An Overview of the HFL Model Checking Project

Naoki Kobayashi
(The University of Tokyo)

In this article, we give an overview of our project on higher-order program verification based on HFL (higher-order fixpoint logic) model checking. After a brief introduction to HFL, we explain how it can be applied to program verification, and summarize the current status of the project.

In Hossein Hojjat and Bishoksan Kafle : Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2021), Virtual, 28th March 2021, Electronic Proceedings in Theoretical Computer Science 344, pp. 1–12.
Published: 13th September 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.344.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org