Automatic HFL(Z) Validity Checking for Program Verification
Programming Languages
2022-12-12 v2
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.
Keywords
Cite
@article{arxiv.2203.07601,
title = {Automatic HFL(Z) Validity Checking for Program Verification},
author = {Naoki Kobayashi and Kento Tanahashi and Ryosuke Sato and Takeshi Tsukada},
journal= {arXiv preprint arXiv:2203.07601},
year = {2022}
}
Comments
A long version of the paper published in Proceedings of POPL 2023