{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:15:35Z","timestamp":1770275735485,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642198045","type":"print"},{"value":"9783642198052","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-19805-2_18","type":"book-chapter","created":{"date-parts":[[2011,3,14]],"date-time":"2011-03-14T09:05:14Z","timestamp":1300093514000},"page":"260-274","source":"Crossref","is-referenced-by-count":21,"title":["A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes"],"prefix":"10.1007","author":[{"given":"Naoki","family":"Kobayashi","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","first-page":"1","volume-title":"Computational Logic: Proceedings of the 1997 Marktoberdorf Summer School","author":"S. Abramsky","year":"1999","unstructured":"Abramsky, S., McCusker, G.: Game semantics. In: Computational Logic: Proceedings of the 1997 Marktoberdorf Summer School, pp. 1\u201356. Springer, Heidelberg (1999)"},{"key":"18_CR2","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"},{"issue":"1","key":"18_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/565816.503274","volume":"37","author":"Thomas Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: Proc. of POPL, pp. 1\u20133 (2002)","journal-title":"ACM SIGPLAN Notices"},{"issue":"5-6","key":"18_CR4","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. International Journal on Software Tools for Technology Transfer\u00a09(5-6), 505\u2013525 (2007)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-24725-8_21","volume-title":"Programming Languages and Systems","author":"S. Carlier","year":"2004","unstructured":"Carlier, S., Polakow, J., Wells, J.B., Kfoury, A.J.: System E: Expansion variables for flexible typing with linear and non-linear types and intersection types. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 294\u2013309. Springer, Heidelberg (2004)"},{"key":"18_CR6","first-page":"452","volume-title":"Proceedings of 23rd Annual IEEE Symposium on Logic in Computer Science","author":"M. Hague","year":"2008","unstructured":"Hague, M., Murawski, A., Ong, C.-H.L., Serre, O.: Collapsible pushdown automata and recursion schemes. In: Proceedings of 23rd Annual IEEE Symposium on Logic in Computer Science, pp. 452\u2013461. IEEE Computer Society, Los Alamitos (2008)"},{"issue":"1-3","key":"18_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2003.10.032","volume":"311","author":"A.J. Kfoury","year":"2004","unstructured":"Kfoury, A.J., Wells, J.B.: Principality and type inference for intersection types using expansion variables. Theor. Comput. Sci.\u00a0311(1-3), 1\u201370 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-45413-6_21","volume-title":"Typed Lambda Calculi and Applications","author":"T. Knapik","year":"2001","unstructured":"Knapik, T., Niwinski, D., Urzyczyn, P.: Deciding monadic theories of hyperalgebraic trees. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol.\u00a02044, pp. 253\u2013267. Springer, Heidelberg (2001)"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/3-540-45931-6_15","volume-title":"Foundations of Software Science and Computation Structures","author":"T. Knapik","year":"2002","unstructured":"Knapik, T., Niwinski, 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)"},{"key":"18_CR10","first-page":"25","volume-title":"Proceedings of PPDP 2009","author":"N. Kobayashi","year":"2009","unstructured":"Kobayashi, N.: Model-checking higher-order functions. In: Proceedings of PPDP 2009, pp. 25\u201336. ACM Press, New York (2009), see also [13]"},{"key":"18_CR11","unstructured":"Kobayashi, N.: TRecS (2009), \n                    \n                      http:\/\/www.kb.ecei.tohoku.ac.jp\/~koba\/trecs\/"},{"issue":"1","key":"18_CR12","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1145\/1594834.1480933","volume":"44","author":"Naoki Kobayashi","year":"2009","unstructured":"Kobayashi, N.: Types and higher-order recursion schemes for verification of higherorder programs. In: Proc. of POPL, pp. 416\u2013428 (2009), see also [13]","journal-title":"ACM SIGPLAN Notices"},{"key":"18_CR13","unstructured":"Kobayashi, N.: Model checking higher-order programs. A revised and extended version of [12] and [10], available from the author\u2019s web page (2010)"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes (2010), an extended version \n                    \n                      http:\/\/www.kb.ecei.tohoku.ac.jp\/~koba\/gtrecs\/","DOI":"10.1007\/978-3-642-19805-2_18"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-642-02930-1_19","volume-title":"Automata, Languages and Programming","author":"N. Kobayashi","year":"2009","unstructured":"Kobayashi, N., Ong, C.-H.L.: Complexity of model checking recursion schemes for fragments of the modal mu-calculus. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol.\u00a05556, pp. 223\u2013234. Springer, Heidelberg (2009)"},{"key":"18_CR16","first-page":"179","volume-title":"Proceedings of LICS 2009","author":"N. Kobayashi","year":"2009","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, Los Alamitos (2009)"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and cegar for higher-order model checking (July 2010) (unpublished manuscript)","DOI":"10.1145\/1993498.1993525"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: Proc. of POPL, pp. 495\u2013508 (2010)","DOI":"10.1145\/1707801.1706355"},{"key":"18_CR19","unstructured":"Lester, M.M., Neatherway, R.P., Ong, C.-H.L., Ramsay, S.J.: Model checking liveness properties of higher-order functional programs (2010) (unpublished manuscript)"},{"key":"18_CR20","first-page":"81","volume-title":"LICS 2006","author":"C.-H.L. Ong","year":"2006","unstructured":"Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS 2006, pp. 81\u201390. IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"18_CR21","unstructured":"Ong, C.-H.L., Ramsay, S.: Verifying higher-order programs with pattern-matching algebraic data types. In: Proceedings of POPL 2011 (to appear, 2011)"},{"issue":"2","key":"18_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"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19805-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T06:37:32Z","timestamp":1558420652000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19805-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642198045","9783642198052"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19805-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}