@inproceedings{10.1007/978-3-319-89884-1_25,
    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.},
    Address = {Cham},
    Author = {Kobayashi, Naoki and Tsukada, Takeshi and Watanabe, Keiichi},
    BookTitle = {Programming Languages and Systems},
    Editor = {Ahmed, Amal},
    ISBN = {978-3-319-89884-1},
    Pages = {711--738},
    Publisher = {Springer International Publishing},
    Title = {Higher-Order Program Verification via HFL Model Checking},
    Year = {2018},
    date-added = {2018-10-30 10:49:20 +0100},
    date-modified = {2018-10-30 10:49:20 +0100},
    doi = {10.1007/978-3-319-89884-1_25}
}

@inproceedings{10.1007/978-3-319-89884-1_25, 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.}, Address = {Cham}, Author = {Kobayashi, Naoki and Tsukada, Takeshi and Watanabe, Keiichi}, BookTitle = {Programming Languages and Systems}, Editor = {Ahmed, Amal}, ISBN = {978-3-319-89884-1}, Pages = {711--738}, Publisher = {Springer International Publishing}, Title = {Higher-Order Program Verification via HFL Model Checking}, Year = {2018}, date-added = {2018-10-30 10:49:20 +0100}, date-modified = {2018-10-30 10:49:20 +0100}, doi = {10.1007/978-3-319-89884-1_25} }