References

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