{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:16:35Z","timestamp":1770272195052,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642315848","type":"print"},{"value":"9783642315855","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31585-5_18","type":"book-chapter","created":{"date-parts":[[2012,6,23]],"date-time":"2012-06-23T11:56:29Z","timestamp":1340452589000},"page":"165-176","source":"Crossref","is-referenced-by-count":24,"title":["A Saturation Method for Collapsible Pushdown Systems"],"prefix":"10.1007","author":[{"given":"Chris","family":"Broadbent","sequence":"first","affiliation":[]},{"given":"Arnaud","family":"Carayol","sequence":"additional","affiliation":[]},{"given":"Matthew","family":"Hague","sequence":"additional","affiliation":[]},{"given":"Olivier","family":"Serre","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"Atig, M.F.: Global model checking of ordered multi-pushdown systems. In: FSTTCS, pp. 216\u2013227 (2010)"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: POPL, pp. 1\u20133 (2002)","DOI":"10.1145\/565816.503274"},{"key":"18_CR3","unstructured":"Benois, M.: Parties rationnelles du groupe libre. Comptes-Rendus de l\u2019Acamd\u00e9mie des Sciences de Paris, S\u00e9rie A, 1188\u20131190 (1969)"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pushdown Automata: Application to Model-Checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-30538-5_12","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"A. Bouajjani","year":"2004","unstructured":"Bouajjani, A., Meyer, A.: Symbolic Reachability Analysis of Higher-Order Context-Free Processes. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 135\u2013147. Springer, Heidelberg (2004)"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Broadbent, C.H., Carayol, A., Ong, C.-H.L., Serre, O.: Recursion schemes and logical reflection. In: LiCS, pp. 120\u2013129 (2010)","DOI":"10.1109\/LICS.2010.40"},{"key":"18_CR7","unstructured":"Cachat, T.: Games on Pushdown Graphs and Extensions. PhD thesis, RWTH Aachen (2003)"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/11549345_16","volume-title":"Mathematical Foundations of Computer Science 2005","author":"A. Carayol","year":"2005","unstructured":"Carayol, A.: Regular Sets of Higher-Order Pushdown Stacks. In: Jedrzejowicz, J., Szepietowski, A. (eds.) MFCS 2005. LNCS, vol.\u00a03618, pp. 168\u2013179. Springer, Heidelberg (2005)"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-540-24597-1_10","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"A. Carayol","year":"2003","unstructured":"Carayol, A., W\u00f6hrle, S.: The Caucal Hierarchy of Infinite Graphs in Terms of Logic and Higher-Order Pushdown Automata. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 112\u2013123. Springer, Heidelberg (2003)"},{"issue":"1","key":"18_CR10","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A.K. Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D., Stockmeyer, L.J.: Alternation. J. ACM\u00a028(1), 114\u2013133 (1981)","journal-title":"J. ACM"},{"key":"18_CR11","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0304-3975(82)90009-3","volume":"20","author":"W. Damm","year":"1982","unstructured":"Damm, W.: The IO- and OI-hierarchies. Theor. Comput. Sci.\u00a020, 95\u2013207 (1982)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient Algorithms for Model Checking Pushdown Systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 232\u2013247. Springer, Heidelberg (2000)"},{"key":"18_CR13","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/S1571-0661(05)80426-8","volume":"9","author":"A. Finkel","year":"1997","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Electr. Notes Theor. Comput. Sci.\u00a09, 27\u201337 (1997)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Hague, M., Murawski, A.S., Ong, C.-H.L., Serre, O.: Collapsible pushdown automata and recursion schemes. In: LiCS, pp. 452\u2013461 (2008)","DOI":"10.1109\/LICS.2008.34"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Hague, M., Ong, C.-H.L.: Symbolic backwards-reachability analysis for higher-order pushdown systems. Logical Methods in Computer Science 4(4) (2008)","DOI":"10.2168\/LMCS-4(4:14)2008"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-16164-3_14","volume-title":"Model Checking Software","author":"M. Hague","year":"2010","unstructured":"Hague, M., Ong, C.-H.L.: Analysing Mu-Calculus Properties of Pushdown Systems. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol.\u00a06349, pp. 187\u2013192. Springer, Heidelberg (2010)"},{"issue":"5","key":"18_CR17","doi-asserted-by":"publisher","first-page":"799","DOI":"10.1016\/j.ic.2010.12.004","volume":"209","author":"M. Hague","year":"2010","unstructured":"Hague, M., Ong, C.-H.L.: A saturation method for the modal \u03bc-calculus over pushdown systems. Inf. Comput.\u00a0209(5), 799\u2013821 (2010)","journal-title":"Inf. Comput."},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Kartzow, A., Parys, P.: Strictness of the Collapsible Pushdown Hierarchy. arXiv:1201.3250v1 [cs.FL] (2012)","DOI":"10.1007\/978-3-642-32589-2_50"},{"key":"18_CR19","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., 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)"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1450","DOI":"10.1007\/11523468_117","volume-title":"Automata, Languages and Programming","author":"T. Knapik","year":"2005","unstructured":"Knapik, T., Niwi\u0144ski, D., Urzyczyn, P., Walukiewicz, I.: Unsafe Grammars and Panic Automata. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 1450\u20131461. Springer, Heidelberg (2005)"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Higher-order model checking: From theory to practice. In: LiCS, pp. 219\u2013224 (2011)","DOI":"10.1109\/LICS.2011.15"},{"key":"18_CR22","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":"18_CR23","first-page":"1170","volume":"15","author":"A.N. Maslov","year":"1976","unstructured":"Maslov, A.N.: Multilevel stack automata. Problems of Information Transmission\u00a015, 1170\u20131174 (1976)","journal-title":"Problems of Information Transmission"},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: LiCS, pp. 81\u201390 (2006)","DOI":"10.1109\/LICS.2006.38"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Ong, C.-H.L., Ramsay, S.J.: Verifying higher-order functional programs with pattern-matching algebraic data types. In: POPL, pp. 587\u2013598 (2011)","DOI":"10.1145\/1925844.1926453"},{"key":"18_CR26","unstructured":"Parys, P.: Collapse operation increases expressive power of deterministic higher order pushdown automata. In: STACS, pp. 603\u2013614 (2011)"},{"issue":"1-2","key":"18_CR27","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1016\/j.scico.2005.02.009","volume":"58","author":"T.W. Reps","year":"2005","unstructured":"Reps, T.W., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program.\u00a058(1-2), 206\u2013263 (2005)","journal-title":"Sci. Comput. Program."},{"key":"18_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-22012-8_12","volume-title":"Automata, Languages and Programming","author":"S. Salvati","year":"2011","unstructured":"Salvati, S., Walukiewicz, I.: Krivine Machines and Higher-Order Schemes. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol.\u00a06756, pp. 162\u2013173. Springer, Heidelberg (2011)"},{"key":"18_CR29","unstructured":"Schwoon, S.: Model-checking Pushdown Systems. PhD thesis, Technical University of Munich (2002)"},{"key":"18_CR30","unstructured":"Seth, A.: An alternative construction in symbolic reachability analysis of second order pushdown systems. In: RP, pp. 80\u201395 (2007)"},{"key":"18_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-642-04420-5_19","volume-title":"Reachability Problems","author":"A. Seth","year":"2009","unstructured":"Seth, A.: Games on Higher Order Multi-stack Pushdown Systems. In: Bournez, O., Potapov, I. (eds.) RP 2009. LNCS, vol.\u00a05797, pp. 203\u2013216. Springer, Heidelberg (2009)"},{"key":"18_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-540-85114-1_19","volume-title":"Model Checking Software","author":"D. Suwimonteerabuth","year":"2008","unstructured":"Suwimonteerabuth, D., Esparza, J., Schwoon, S.: Symbolic Context-Bounded Analysis of Multithreaded Java Programs. In: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 270\u2013287. Springer, Heidelberg (2008)"},{"key":"18_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/11901914_13","volume-title":"Automated Technology for Verification and Analysis","author":"D. Suwimonteerabuth","year":"2006","unstructured":"Suwimonteerabuth, D., Schwoon, S., Esparza, J.: Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 141\u2013153. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages, and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31585-5_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T13:50:20Z","timestamp":1743601820000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31585-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642315848","9783642315855"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31585-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}