{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,29]],"date-time":"2025-03-29T04:10:24Z","timestamp":1743221424093,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642298219"},{"type":"electronic","value":"9783642298226"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-29822-6_22","type":"book-chapter","created":{"date-parts":[[2012,5,20]],"date-time":"2012-05-20T13:21:09Z","timestamp":1337520069000},"page":"275-289","source":"Crossref","is-referenced-by-count":9,"title":["Exact Flow Analysis by Higher-Order Model Checking"],"prefix":"10.1007","author":[{"given":"Yoshihiro","family":"Tobita","sequence":"first","affiliation":[]},{"given":"Takeshi","family":"Tsukada","sequence":"additional","affiliation":[]},{"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-540-89330-1_20","volume-title":"Programming Languages and Systems","author":"M. Blume","year":"2008","unstructured":"Blume, M., Acar, U.A., Chae, W.: Exception Handlers as Extensible Cases. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol.\u00a05356, pp. 273\u2013289. Springer, Heidelberg (2008)"},{"issue":"4","key":"22_CR2","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1017\/S0960129500001535","volume":"2","author":"O. Danvy","year":"1992","unstructured":"Danvy, O., Filinski, A.: Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science\u00a02(4), 361\u2013391 (1992)","journal-title":"Mathematical Structures in Computer Science"},{"key":"22_CR3","unstructured":"Earl, C., Might, M., Horn, D.V.: Pushdown control-flow analysis of higher-order programs. CoRR abs\/1007.4268 (2010)"},{"issue":"5","key":"22_CR4","doi-asserted-by":"publisher","first-page":"823","DOI":"10.1017\/S0960129508006968","volume":"18","author":"M. F\u00e4hndrich","year":"2008","unstructured":"F\u00e4hndrich, M., Rehof, J.: Type-based flow analysis and context-free language reachability. Mathematical Structures in Computer Science\u00a018(5), 823\u2013894 (2008)","journal-title":"Mathematical Structures in Computer Science"},{"key":"22_CR5","doi-asserted-by":"crossref","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 (2008)","DOI":"10.1109\/LICS.2008.34"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Heintze, N., McAllester, D.: Linear-time subtransitive control flow analysis. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 261\u2013272 (1997)","DOI":"10.1145\/258916.258939"},{"key":"22_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":"22_CR8","unstructured":"Kobayashi, N.: TRecS: A type-based model checker for recursion schemes (2009), http:\/\/www.kb.ecei.tohoku.ac.jp\/~koba\/trecs\/"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: Proceedings of POPL, pp. 416\u2013428 (2009)","DOI":"10.1145\/1594834.1480933"},{"key":"22_CR10","unstructured":"Kobayashi, N.: Model checking higher-order programs. Submitted for publication. A revised and extended version of [9] and [7] (2010), http:\/\/www.kb.ecei.tohoku.ac.jp\/~koba\/papers\/hmc.pdf"},{"key":"22_CR11","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":"22_CR12","series-title":"LNCS","first-page":"275","volume-title":"FLOPS 2012","author":"N. Kobayashi","year":"2012","unstructured":"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)"},{"key":"22_CR13","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":"22_CR14","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)","DOI":"10.1145\/1993498.1993525"},{"key":"22_CR15","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, pp. 495\u2013508 (2010)","DOI":"10.1145\/1707801.1706355"},{"key":"22_CR16","unstructured":"Lester, M.M., Neatherway, R.P., Ong, C.-H.L., Ramsay, S.J.: THORS hammer (2011), http:\/\/mjolnir.cs.ox.ac.uk\/thors"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/3-540-15648-8_17","volume-title":"Logics of Programs","author":"A.R. Meyer","year":"1985","unstructured":"Meyer, A.R., Wand, M.: Continuation Semantics in Typed Lambda-calculi (Summary). In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol.\u00a0193, pp. 219\u2013224. Springer, Heidelberg (1985)"},{"issue":"1","key":"22_CR18","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1017\/S0960129502003857","volume":"13","author":"C. Mossin","year":"2003","unstructured":"Mossin, C.: Exact flow analysis. Mathematical Structures in Computer Science\u00a013(1), 125\u2013156 (2003)","journal-title":"Mathematical Structures in Computer Science"},{"key":"22_CR19","doi-asserted-by":"crossref","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 (2006)","DOI":"10.1109\/LICS.2006.38"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Ong, C.-H.L., Tzevelekos, N.: Functional reachability. In: Proceedings of LICS, pp. 286\u2013295. IEEE Computer Society (2009)","DOI":"10.1109\/LICS.2009.48"},{"issue":"2","key":"22_CR21","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G.D. Plotkin","year":"1975","unstructured":"Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science\u00a01(2), 125\u2013159 (1975)","journal-title":"Theoretical Computer Science"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Prabhu, T., Ramalingam, S., Might, M., Hall, M.W.: EigenCFA: accelerating flow analysis with gpus. In: Proceedings of POPL, pp. 511\u2013522 (2011)","DOI":"10.1145\/1925844.1926445"},{"key":"22_CR23","unstructured":"Shivers, O.: Control-Flow Analysis of Higher-Order Languages. Ph.D. thesis, Carnegie-Mellon University (May 1991)"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Shivers, O.: Higher-order control-flow analysis in retrospect: Lessons learned, lessons abandoned. In: ACM SIGPLAN Notices - Best of PLDI 1979-1999, pp. 257\u2013269 (2003)","DOI":"10.1145\/989393.989421"},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"Vardoulakis, D., Shivers, O.: CFA2: a context-free approach to control-flow analysis. Logical Methods in Computer Science\u00a07(2) (2011)","DOI":"10.2168\/LMCS-7(2:3)2011"},{"key":"22_CR26","doi-asserted-by":"crossref","unstructured":"Vardoulakis, D., Shivers, O.: Pushdown flow analysis of first-class control. In: Proceedings of ICFP, pp. 69\u201380. ACM Press (2011)","DOI":"10.1145\/2034574.2034785"},{"issue":"1","key":"22_CR27","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1145\/271510.271523","volume":"20","author":"A.K. Wright","year":"1998","unstructured":"Wright, A.K., Jagannathan, S.: Polymorphic splitting: An effective polyvariant flow analysis. TOPLAS\u00a020(1), 166\u2013207 (1998)","journal-title":"TOPLAS"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-29822-6_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T10:22:10Z","timestamp":1743157330000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-29822-6_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642298219","9783642298226"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-29822-6_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}