Keiichi Watanabe
A Software Engineer at Google
Research Areas
Authored Publications
Sort By
Reduction from Branching-time Property Verification of Higher-Order Programs to HFL Validity Checking
Hiroki Oshikawa
Naoki Kobayashi
Takeshi Tsukada
43rd International Symposium on Mathematical Foundations of Computer Science (2019)
Preview abstract
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.
View details
