Higher-Order Program Verification via HFL Model Checking

Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe

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…