Automatic HFL(Z) Validity Checking for Program Verification

TL;DR

This paper introduces an automated approach for verifying the validity of HFL(Z) formulas, enabling comprehensive and automated verification of complex temporal properties in higher-order functional programs.

Contribution

It presents a fully automated, uniform verification method for higher-order program properties by combining HFL(Z) validity checking with existing reduction techniques.

Findings

Implemented the proposed method with promising experimental results.

Successfully verified various temporal properties including termination and fairness.

Demonstrated the method's applicability to complex higher-order programs.

Abstract

We propose an automated method for checking the validity of a formula of HFL(Z), a higher-order logic with fixpoint operators and integers. Combined with Kobayashi et al.'s reduction from higher-order program verification to HFL(Z) validity checking, our method yields a fully automated, uniform verification method for arbitrary temporal properties of higher-order functional programs expressible in the modal mu-calculus, including termination, non-termination, fair termination, fair non-termination, and also branching-time properties. We have implemented our method and obtained promising experimental results.