Higher-Order Program Verification via HFL Model Checking
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.
Cite
@article{arxiv.1710.08614,
title = {Higher-Order Program Verification via HFL Model Checking},
author = {Naoki Kobayashi and Takeshi Tsukada and Keiichi Watanabe},
journal= {arXiv preprint arXiv:1710.08614},
year = {2018}
}
Comments
A shorter version is published in Proceedings of ESOP 2018