{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T04:10:09Z","timestamp":1746418209805,"version":"3.40.4"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319127354"},{"type":"electronic","value":"9783319127361"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-12736-1_19","type":"book-chapter","created":{"date-parts":[[2014,10,13]],"date-time":"2014-10-13T14:53:24Z","timestamp":1413212004000},"page":"354-371","source":"Crossref","is-referenced-by-count":5,"title":["A ZDD-Based Efficient Higher-Order Model Checking Algorithm"],"prefix":"10.1007","author":[{"given":"Taku","family":"Terao","sequence":"first","affiliation":[]},{"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Aehlig, K.: A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science\u00a03(3) (2007)","DOI":"10.2168\/LMCS-3(3:1)2007"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Broadbent, C.H., Carayol, A., Hague, M., Serre, O.: C-SHORe: A collapsible approach to higher-order verification. In: Proceedings of ICFP 2013, pp. 13\u201324 (2013)","DOI":"10.1145\/2544174.2500589"},{"key":"19_CR3","unstructured":"Broadbent, C.H., Kobayashi, N.: Saturation-based model checking of higher-order recursion schemes. In: Proceedings of CSL 2013. LIPIcs, vol.\u00a023, pp. 129\u2013148 (2013)"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-03542-0_2","volume-title":"Programming Languages and Systems","author":"K. Fujima","year":"2013","unstructured":"Fujima, K., Ito, S., Kobayashi, N.: Practical alternating parity tree automata model checking of higher-order recursion schemes. In: Shan, C.-C. (ed.) APLAS 2013. LNCS, vol.\u00a08301, pp. 17\u201332. Springer, Heidelberg (2013)"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Heintze, N., McAllester, D.A.: Linear-time subtransitive control flow analysis. In: Proceedings of PLDI 1997, pp. 261\u2013272 (1997)","DOI":"10.1145\/258916.258939"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Knapik, T., Niwi\u0144ski, D., Urzyczyn, P.: Higher-order pushdown trees are easy. In: Nielsen, M., Engberg, U. (eds.) Fossacs 2002. LNCS, vol.\u00a02303, pp. 205\u2013222. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45931-6_15"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Model-checking higher-order functions. In: Proceedings of PPDP 2009, pp. 25\u201336. ACM Press (2009)","DOI":"10.1145\/1599410.1599415"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-19805-2_18","volume-title":"Foundations of Software Science and Computational Structures","author":"N. Kobayashi","year":"2011","unstructured":"Kobayashi, N.: A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol.\u00a06604, pp. 260\u2013274. Springer, Heidelberg (2011)"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Model checking higher-order programs. Journal of the ACM\u00a060(3) (2013)","DOI":"10.1145\/2487241.2487246"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Ong, C.-H.L.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: Proceedings of LICS 2009, pp. 179\u2013188. IEEE Computer Society Press (2009)","DOI":"10.1109\/LICS.2009.29"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Ong, C.-H.L.: Complexity of model checking recursion schemes for fragments of the modal mu-calculus. Logical Methods in Computer Science\u00a07(4) (2011)","DOI":"10.2168\/LMCS-7(4:9)2011"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of PLDI 2011, pp. 222\u2013233. ACM Press (2011)","DOI":"10.1145\/1993316.1993525"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: Proceedings of POPL 2010, pp. 495\u2013508. ACM Press (2010)","DOI":"10.1145\/1707801.1706355"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Kuwahara, T., Terauchi, T., Unno, H., Kobayashi, N.: Automatic termination verification for higher-order functional programs. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol.\u00a08410, pp. 392\u2013411. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54833-8_21"},{"key":"19_CR15","unstructured":"Lester, M.M., Neatherway, R.P., Ong, C.-H.L., Ramsay, S.J.: Model checking liveness properties of higher-order functional programs. In: Proceedings of ML Workshop 2011 (2011)"},{"key":"19_CR16","unstructured":"Midtgaard, J., Horn, D.V.: Subcubic control flow analysis algorithms. Higher-Order and Symbolic Computation"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Minato, S.: Zero-suppressed bdds for set manipulation in combinatorial problems. In: Proceedings of DAC 1993, pp. 272\u2013277 (1993)","DOI":"10.1145\/157485.164890"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Neatherway, R.P., Ramsay, S.J., Ong, C.-H.L.: A traversal-based algorithm for higher-order model checking. In: ACM SIGPLAN International Conference on Functional Programming (ICFP 2012), pp. 353\u2013364 (2012)","DOI":"10.1145\/2398856.2364578"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: Proceedings of LICS 2006, pp. 81\u201390. IEEE Computer Society Press (2006)","DOI":"10.1109\/LICS.2006.38"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Ong, C.-H.L., Ramsay, S.: Verifying higher-order programs with pattern-matching algebraic data types. In: Proceedings of POPL 2011, pp. 587\u2013598. ACM Press (2011)","DOI":"10.1145\/1925844.1926453"},{"key":"19_CR21","doi-asserted-by":"crossref","unstructured":"Ramsay, S., Neatherway, R., Ong, C.-H.L.: An abstraction refinement approach to higher-order model checking. In: Proceedings of POPL 2014 (2014)","DOI":"10.1145\/2535838.2535873"},{"issue":"2","key":"19_CR22","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1016\/S0167-6423(99)00011-8","volume":"35","author":"J. Rehof","year":"1999","unstructured":"Rehof, J., Mogensen, T.: Tractable constraints in finite semilattices. Science of Computer Programming\u00a035(2), 191\u2013221 (1999)","journal-title":"Science of Computer Programming"},{"key":"19_CR23","unstructured":"Shivers, O.: Control-Flow Analysis of Higher-Order Languages. Ph.D. thesis, Carnegie-Mellon University (May 1991)"},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-642-29822-6_22","volume-title":"Functional and Logic Programming","author":"Y. Tobita","year":"2012","unstructured":"Tobita, Y., Tsukada, T., Kobayashi, N.: Exact flow analysis by higher-order model checking. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol.\u00a07294, pp. 275\u2013289. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12736-1_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T03:47:37Z","timestamp":1746416857000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-12736-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319127354","9783319127361"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12736-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}