@article(DBLP:journals/lmcs/AxelssonLS07,
 author       = {Roland Axelsson and Martin Lange and Rafal Somla},
 year         = {2007},
 title        = {The Complexity of Model Checking Higher-Order Fixpoint Logic},
 journal      = {Logical Methods in Computer Science},
 volume       = {3},
 number       = {2},
 doi          = {10.2168/LMCS-3(2:7)2007},
)
@inproceedings(SLAM,
 author       = {Thomas Ball and Byron Cook and Vladimir Levin and Sriram K. Rajamani},
 year         = {2004},
 title        = {{SLAM} and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft},
 booktitle    = {Integrated Formal Methods 2004},
 series       = {LNCS},
 volume       = {2999},
 publisher    = {Springer},
 pages        = {1--20},
 doi          = {10.1007/978-3-540-24756-2\_1},
)
@inproceedings(Bjorner15,
 author       = {Bj{\o}rner, Nikolaj and Arie Gurfinkel and Kenneth L. McMillan and Andrey Rybalchenko},
 year         = {2015},
 title        = {Horn Clause Solvers for Program Verification},
 booktitle    = {Fields of Logic and Computation {II} - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday},
 series       = {LNCS},
 volume       = {9300},
 publisher    = {Springer},
 pages        = {24--51},
 doi          = {10.1007/978-3-319-23534-9\_2},
)
@inproceedings(Kobayashi13horsat,
 author       = {Christopher H. Broadbent and Naoki Kobayashi},
 year         = {2013},
 title        = {Saturation-Based Model Checking of Higher-Order Recursion Schemes},
 booktitle    = {{CSL} 2013},
 series       = {LIPIcs},
 volume       = {23},
 pages        = {129--148},
 doi          = {10.4230/LIPIcs.CSL.2013.129},
)
@article(DBLP:journals/pacmpl/BurnOR18,
 author       = {Toby Cathcart Burn and C.{-}H. Luke Ong and Steven J. Ramsay},
 year         = {2018},
 title        = {Higher-order constrained horn clauses for verification},
 journal      = {Proc. {ACM} Program. Lang.},
 volume       = {2},
 number       = {{POPL}},
 pages        = {11:1--11:28},
 doi          = {10.1145/3158099},
)
@article(DBLP:journals/jar/ChampionCKS20,
 author       = {Adrien Champion and Tomoya Chiba and Naoki Kobayashi and Ryosuke Sato},
 year         = {2020},
 title        = {ICE-Based Refinement Type Discovery for Higher-Order Functional Programs},
 journal      = {J. Autom. Reason.},
 volume       = {64},
 number       = {7},
 pages        = {1393--1418},
 doi          = {10.1007/s10817-020-09571-y},
)
@book(ClarkeModelChecking,
 author       = {Edmund M. Clarke and Orna Grumberg and Doron A. Peled},
 year         = {1999},
 title        = {Model Checking},
 publisher    = {The MIT Press},
)
@inproceedings(Cook07POPL,
 author       = {Byron Cook and Alexey Gotsman and Andreas Podelski and Andrey Rybalchenko and Moshe Y. Vardi},
 year         = {2007},
 title        = {Proving That Programs Eventually Do Something Good},
 booktitle    = {Proceedings of POPL},
 publisher    = {ACM Press},
 pages        = {265--276},
 doi          = {10.1145/1190216.1190257},
)
@inproceedings(Cook2013a,
 author       = {Byron Cook and Eric Koskinen},
 year         = {2013},
 title        = {Reasoning About Nondeterminism in Programs},
 booktitle    = {Proceedings of PLDI 2013},
 publisher    = {ACM Press},
 pages        = {219--230},
 doi          = {10.1145/2491956.2491969},
)
@article(DBLP:journals/tplp/AngelisFPP18a,
 author       = {{De Angelis}, Emanuele and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti},
 year         = {2018},
 title        = {Solving Horn Clauses on Inductive Data Types Without Induction},
 journal      = {{TPLP}},
 volume       = {18},
 number       = {3-4},
 pages        = {452--469},
 doi          = {10.1017/S1471068418000157},
)
@inproceedings(DBLP:conf/cade/AngelisFPP20,
 author       = {{De Angelis}, Emanuele and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti},
 year         = {2020},
 title        = {Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates},
 editor       = {Nicolas Peltier and Sofronie{-}Stokkermans, Viorica},
 booktitle    = {Automated Reasoning - 10th International Joint Conference, {IJCAR} 2020, Paris, France, July 1-4, 2020, Proceedings, Part {I}},
 series       = {Lecture Notes in Computer Science},
 volume       = {12166},
 publisher    = {Springer},
 pages        = {83--102},
 doi          = {10.1007/978-3-030-51074-9\_6},
)
@article(DBLP:journals/sttt/DelzannoP01,
 author       = {Giorgio Delzanno and Andreas Podelski},
 year         = {2001},
 title        = {Constraint-based deductive model checking},
 journal      = {Int. J. Softw. Tools Technol. Transf.},
 volume       = {3},
 number       = {3},
 pages        = {250--270},
 doi          = {10.1007/s100090100049},
)
@article(DBLP:journals/pacmpl/EzudheenND0M18,
 author       = {P. Ezudheen and Daniel Neider and Deepak D'Souza and Pranav Garg and P. Madhusudan},
 year         = {2018},
 title        = {Horn-ICE learning for synthesizing invariants and contracts},
 journal      = {Proc. {ACM} Program. Lang.},
 volume       = {2},
 number       = {{OOPSLA}},
 pages        = {131:1--131:25},
 doi          = {10.1145/3276501},
)
@inproceedings(freqterm,
 author       = {Grigory Fedyukovich and Yueling Zhang and Aarti Gupta},
 year         = {2018},
 title        = {Syntax-Guided Termination Analysis},
 booktitle    = {Computer Aided Verification - 30th International Conference, {CAV} 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part {I}},
 series       = {LNCS},
 volume       = {10981},
 publisher    = {Springer},
 pages        = {124--143},
 doi          = {10.1007/978-3-319-96145-3\_7},
)
@proceedings(Automata,
 editor       = {Erich Gr{\"a}del and Wolfgang Thomas and Thomas Wilke},
 year         = {2002},
 title        = {Automata, Logics, and Infinite Games: A Guide to Current Research},
 series       = {LNCS},
 volume       = {2500},
 publisher    = {Springer},
 doi          = {10.1007/3-540-36387-4},
)
@inproceedings(Eldarica,
 author       = {H. {Hojjat} and {R\IeC{\"u}mmer}, P.},
 year         = {2018},
 title        = {The ELDARICA Horn Solver},
 booktitle    = {2018 Formal Methods in Computer Aided Design (FMCAD)},
 pages        = {1--7},
 doi          = {10.23919/FMCAD.2018.8603013},
)
@inproceedings(DBLP:conf/aplas/Hosoi0T19,
 author       = {Youkichi Hosoi and Naoki Kobayashi and Takeshi Tsukada},
 year         = {2019},
 title        = {A Type-Based {HFL} Model Checking Algorithm},
 editor       = {Anthony Widjaja Lin},
 booktitle    = {Programming Languages and Systems - 17th Asian Symposium, {APLAS} 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {11893},
 publisher    = {Springer},
 pages        = {136--155},
 doi          = {10.1007/978-3-030-34175-6\_8},
)
@inproceedings(DBLP:conf/sas/IwayamaKST20,
 author       = {Naoki Iwayama and Naoki Kobayashi and Ryota Suzuki and Takeshi Tsukada},
 year         = {2020},
 title        = {Predicate Abstraction and {CEGAR} for $\nu$HFL$_Z$ Validity Checking},
 editor       = {David Pichardie and Mihaela Sighireanu},
 booktitle    = {Static Analysis - 27th International Symposium, {SAS} 2020, Virtual Event, November 18-20, 2020, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {12389},
 publisher    = {Springer},
 pages        = {134--155},
 doi          = {10.1007/978-3-030-65474-0\_7},
)
@inproceedings(DBLP:conf/vmcai/JaffarSV06,
 author       = {Joxan Jaffar and Andrew E. Santosa and Razvan Voicu},
 year         = {2006},
 title        = {A {CLP} Method for Compositional and Intermittent Predicate Abstraction},
 booktitle    = {Proceedings of {VMCAI} 2006},
 series       = {Lecture Notes in Computer Science},
 volume       = {3855},
 publisher    = {Springer},
 pages        = {17--32},
 doi          = {10.1007/11609773\_2},
)
@inproceedings(DBLP:conf/aplas/KatsuraIKT20,
 author       = {Hiroyuki Katsura and Naoki Iwayama and Naoki Kobayashi and Takeshi Tsukada},
 year         = {2020},
 title        = {A New Refinement Type System for Automated $\nu$HFL$_Z$ Validity Checking},
 editor       = {Bruno C. d. S. Oliveira},
 booktitle    = {Programming Languages and Systems - 18th Asian Symposium, {APLAS} 2020, Fukuoka, Japan, November 30 - December 2, 2020, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {12470},
 publisher    = {Springer},
 pages        = {86--104},
 doi          = {10.1007/978-3-030-64437-6\_5},
)
@article(Kobayashi13JACM,
 author       = {Naoki Kobayashi},
 year         = {2013},
 title        = {Model Checking Higher-Order Programs},
 journal      = {J. ACM},
 volume       = {60},
 number       = {3},
 doi          = {10.1145/2487241.2487246},
)
@misc(horsat2,
 author       = {Naoki Kobayashi},
 year         = {2016},
 title        = {{HorSat 2}: A Saturation-Based Model Checker for Higher-Order Recursion Schemes},
 url          = {https://github.com/hopv/horsat2},
)
@inproceedings(DBLP:conf/tacas/KobayashiFG20,
 author       = {Naoki Kobayashi and Grigory Fedyukovich and Aarti Gupta},
 year         = {2020},
 title        = {Fold/Unfold Transformations for Fixpoint Logic},
 editor       = {Armin Biere and David Parker},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, {TACAS} 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part {II}},
 series       = {Lecture Notes in Computer Science},
 volume       = {12079},
 publisher    = {Springer},
 pages        = {195--214},
 doi          = {10.1007/978-3-030-45237-7\_12},
)
@inproceedings(Kobayashi17POPL,
 author       = {Naoki Kobayashi and {\'{E}}tienne Lozes and Florian Bruse},
 year         = {2017},
 title        = {On the relationship between higher-order recursion schemes and higher-order fixpoint logic},
 booktitle    = {{POPL} 2017},
 pages        = {246--259},
 doi          = {10.1145/3009837.3009854},
)
@inproceedings(DBLP:conf/sas/0001NIU19,
 author       = {Naoki Kobayashi and Takeshi Nishikawa and Atsushi Igarashi and Hiroshi Unno},
 year         = {2019},
 title        = {Temporal Verification of Programs via First-Order Fixpoint Logic},
 editor       = {Bor{-}Yuh Evan Chang},
 booktitle    = {Static Analysis - 26th International Symposium, {SAS} 2019, Porto, Portugal, October 8-11, 2019, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {11822},
 publisher    = {Springer},
 pages        = {413--436},
 doi          = {10.1007/978-3-030-32304-2\_20},
)
@inproceedings(KSU11PLDI,
 author       = {Naoki Kobayashi and Ryosuke Sato and Hiroshi Unno},
 year         = {2011},
 title        = {Predicate Abstraction and {CEGAR} for Higher-Order Model Checking},
 booktitle    = {{PLDI} 2011},
 publisher    = {ACM Press},
 pages        = {222--233},
 doi          = {10.1145/1993498.1993525},
)
@inproceedings(KTW18ESOP,
 author       = {Naoki Kobayashi and Takeshi Tsukada and Keiichi Watanabe},
 year         = {2018},
 title        = {Higher-Order Program Verification via {HFL} Model Checking},
 editor       = {Amal Ahmed},
 booktitle    = {Programming Languages and Systems - 27th European Symposium on Programming, {ESOP} 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {10801},
 publisher    = {Springer},
 pages        = {711--738},
 doi          = {10.1007/978-3-319-89884-1\_25},
)
@article(DBLP:journals/fmsd/KomuravelliGC16,
 author       = {Anvesh Komuravelli and Arie Gurfinkel and Sagar Chaki},
 year         = {2016},
 title        = {SMT-based model checking for recursive programs},
 journal      = {Formal Methods Syst. Des.},
 volume       = {48},
 number       = {3},
 pages        = {175--205},
 doi          = {10.1007/s10703-016-0249-4},
)
@inproceedings(DBLP:conf/csl/KoriT021,
 author       = {Mayuko Kori and Takeshi Tsukada and Naoki Kobayashi},
 year         = {2021},
 title        = {A Cyclic Proof System for HFL$_N$},
 editor       = {Christel Baier and Goubault{-}Larrecq, Jean},
 booktitle    = {29th {EACSL} Annual Conference on Computer Science Logic, {CSL} 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference)},
 series       = {LIPIcs},
 volume       = {183},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 pages        = {29:1--29:22},
 doi          = {10.4230/LIPIcs.CSL.2021.29},
)
@article(Kozen83,
 author       = {Dexter Kozen},
 year         = {1983},
 title        = {Results on the Propositional $\mu$-calculus},
 journal      = {{Theoretical Computer Science}},
 volume       = {27},
 pages        = {333--354},
 doi          = {10.1016/0304-3975(82)90125-6},
)
@inproceedings(Kuwahara2015Nonterm,
 author       = {Takuya Kuwahara and Ryosuke Sato and Hiroshi Unno and Naoki Kobayashi},
 year         = {2015},
 title        = {Predicate Abstraction and {CEGAR} for Disproving Termination of Higher-Order Functional Programs},
 booktitle    = {Proceedings of CAV 2015},
 series       = {LNCS},
 volume       = {9207},
 publisher    = {Springer},
 pages        = {287--303},
 doi          = {10.1007/978-3-319-21668-3\_17},
)
@inproceedings(Kuwahara2014Termination,
 author       = {Takuya Kuwahara and Tachio Terauchi and Hiroshi Unno and Naoki Kobayashi},
 year         = {2014},
 title        = {Automatic Termination Verification for Higher-Order Functional Programs},
 booktitle    = {Proceedings of {ESOP} 2014},
 series       = {LNCS},
 volume       = {8410},
 publisher    = {Springer},
 pages        = {392--411},
 doi          = {10.1007/978-3-642-54833-8\_21},
)
@inproceedings(DBLP:conf/popl/MuraseT0SU16,
 author       = {Akihiro Murase and Tachio Terauchi and Naoki Kobayashi and Ryosuke Sato and Hiroshi Unno},
 year         = {2016},
 title        = {Temporal verification of higher-order functional programs},
 editor       = {Bod{\'{\i}}k, Rastislav and Rupak Majumdar},
 booktitle    = {Proceedings of the 43rd Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2016, St. Petersburg, FL, USA, January 20 - 22, 2016},
 publisher    = {{ACM}},
 pages        = {57--68},
 doi          = {10.1145/2837614.2837667},
)
@inproceedings(Ong06LICS,
 author       = {C.-H. Luke Ong},
 year         = {2006},
 title        = {On Model-Checking Trees Generated by Higher-Order Recursion Schemes},
 booktitle    = {{LICS} 2006},
 publisher    = {IEEE Computer Society Press},
 pages        = {81--90},
 doi          = {10.1109/LICS.2006.38},
)
@inproceedings(DBLP:conf/lics/OngW19,
 author       = {C.{-}H. Luke Ong and Dominik Wagner},
 year         = {2019},
 title        = {HoCHC: {A} Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories},
 booktitle    = {34th Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS} 2019, Vancouver, BC, Canada, June 24-27, 2019},
 publisher    = {{IEEE}},
 pages        = {1--14},
 doi          = {10.1109/LICS.2019.8785784},
)
@inproceedings(DBLP:conf/sas/PeraltaGS98,
 author       = {Julio C. Peralta and John P. Gallagher and H{\"{u}}seyin Saglam},
 year         = {1998},
 title        = {Analysis of Imperative Programs through Analysis of Constraint Logic Programs},
 booktitle    = {Proceedings of {SAS} '98},
 series       = {Lecture Notes in Computer Science},
 volume       = {1503},
 publisher    = {Springer},
 pages        = {246--261},
 doi          = {10.1007/3-540-49727-7\_15},
)
@inproceedings(DBLP:conf/lics/PodelskiR04,
 author       = {Andreas Podelski and Andrey Rybalchenko},
 year         = {2004},
 title        = {Transition Invariants},
 booktitle    = {19th {IEEE} Symposium on Logic in Computer Science {(LICS} 2004), 14-17 July 2004, Turku, Finland, Proceedings},
 pages        = {32--41},
 doi          = {10.1109/LICS.2004.1319598},
)
@inproceedings(Jhala08,
 author       = {Patrick M. Rondon and Ming Kawaguchi and Ranjit Jhala},
 year         = {2008},
 title        = {Liquid types},
 booktitle    = {PLDI 2008},
 pages        = {159--169},
 doi          = {10.1145/1375581.1375602},
)
@inproceedings(DBLP:conf/aaai/Satake0Y20,
 author       = {Yuki Satake and Hiroshi Unno and Hinata Yanagi},
 year         = {2020},
 title        = {Probabilistic Inference for Predicate Constraint Satisfaction},
 booktitle    = {The Thirty-Fourth {AAAI} Conference on Artificial Intelligence, {AAAI} 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, {IAAI} 2020, The Tenth {AAAI} Symposium on Educational Advances in Artificial Intelligence, {EAAI} 2020, New York, NY, USA, February 7-12, 2020},
 publisher    = {{AAAI} Press},
 pages        = {1644--1651},
 doi          = {10.1609/aaai.v34i02.5526},
)
@inproceedings(DBLP:conf/lics/Tsukada20,
 author       = {Takeshi Tsukada},
 year         = {2020},
 title        = {On Computability of Logical Approaches to Branching-Time Property Verification of Programs},
 editor       = {Holger Hermanns and Lijun Zhang and Naoki Kobayashi and Dale Miller},
 booktitle    = {{LICS} '20: 35th Annual {ACM/IEEE} Symposium on Logic in Computer Science, Saarbr{\"{u}}cken, Germany, July 8-11, 2020},
 publisher    = {{ACM}},
 pages        = {886--899},
 doi          = {10.1145/3373718.3394766},
)
@inproceedings(Unno09PPDP,
 author       = {Hiroshi Unno and Naoki Kobayashi},
 year         = {2009},
 title        = {Dependent type inference with interpolants},
 booktitle    = {Proceedings of the 11th International {ACM} {SIGPLAN} Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal},
 publisher    = {{ACM}},
 pages        = {277--288},
 doi          = {10.1145/1599410.1599445},
)
@inproceedings(DBLP:conf/popl/UnnoTK13,
 author       = {Hiroshi Unno and Tachio Terauchi and Naoki Kobayashi},
 year         = {2013},
 title        = {Automating relatively complete verification of higher-order functional programs},
 editor       = {Roberto Giacobazzi and Radhia Cousot},
 booktitle    = {The 40th Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} '13, Rome, Italy - January 23 - 25, 2013},
 publisher    = {{ACM}},
 pages        = {75--86},
 doi          = {10.1145/2429069.2429081},
)
@inproceedings(Viswanathan04,
 author       = {M. Viswanathan and R. Viswanathan},
 year         = {2004},
 title        = {A Higher Order Modal Fixed Point Logic},
 booktitle    = {CONCUR},
 series       = {LNCS},
 volume       = {3170},
 publisher    = {Springer},
 pages        = {512--528},
 doi          = {10.1007/978-3-540-28644-8_33},
)
@inproceedings(DBLP:conf/pepm/WatanabeTO019,
 author       = {Keiichi Watanabe and Takeshi Tsukada and Hiroki Oshikawa and Naoki Kobayashi},
 year         = {2019},
 title        = {Reduction from branching-time property verification of higher-order programs to {HFL} validity checking},
 editor       = {Manuel V. Hermenegildo and Atsushi Igarashi},
 booktitle    = {Proceedings of the 2019 {ACM} {SIGPLAN} Workshop on Partial Evaluation and Program Manipulation, PEPM@POPL 2019, Cascais, Portugal, January 14-15, 2019},
 publisher    = {{ACM}},
 pages        = {22--34},
 doi          = {10.1145/3294032.3294077},
)
@inproceedings(Hongwei99POPL,
 author       = {Hongwei Xi and Frank Pfenning},
 year         = {1999},
 title        = {Dependent Types in Practical Programming},
 booktitle    = {Proceedings of POPL},
 pages        = {214--227},
 doi          = {10.1145/292540.292560},
)