An Overview of the HFL Model Checking Project

TL;DR

This paper provides an overview of a project focused on using higher-order fixpoint logic (HFL) for model checking to verify higher-order programs, highlighting the approach and current progress.

Contribution

It introduces the application of HFL model checking to higher-order program verification and summarizes the project's current development status.

Findings

HFL can be effectively applied to higher-order program verification.

The project has made progress in implementing HFL model checking techniques.

The overview sets the stage for future research in higher-order program analysis.

Abstract

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.