Reduction from Branching-time Property Verification of Higher-Order Programs to HFL Validity Checking

Various methods have recently been proposed for temporal property verification of higher-order programs. In those methods, however, either temporal properties were limited to linear-time ones, or target programs were limited to finite-data programs. In this paper, we extend Kobayashi et al.’s recent method for verification of linear-time temporal properties based on HFLz model checking, to deal with branching-time properties. We formalize branching-time property verification problems as an extension of HORS model checking called HORSz model checking, present a sound and complete reduction to validity checking of (modal-free) HFLz formulas, and prove its correctness. The correctness of the reduction subsumes the decidability of HORS model checking. The HFLz formula obtained by the reduction from a HORSz model checking problem can be considered a kind of verification condition for the orignal model checking problem. We also discuss interactive and automated methods for discharging the verification condition.

• Software Systems

• Algorithms and Theory