{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T16:14:37Z","timestamp":1787501677052,"version":"build-2736575974"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540677703","type":"print"},{"value":"9783540450474","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722167_20","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T22:00:33Z","timestamp":1167429633000},"page":"232-247","source":"Crossref","is-referenced-by-count":184,"title":["Efficient Algorithms for Model Checking Pushdown Systems"],"prefix":"10.1007","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Hansel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"Rossmanith","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefan","family":"Schwoon","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"2","key":"20_CR2","first-page":"89","volume":"2","author":"O. Burkart","year":"1995","unstructured":"Burkart, O., Steffen, B.: Composition, decomposition and model checking of pushdown processes. Nordic Journal of Computing\u00a02(2), 89\u2013125 (1995)","journal-title":"Nordic Journal of Computing"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/3-540-63165-8_198","volume-title":"Automata, Languages and Programming","author":"O. Burkart","year":"1997","unstructured":"Burkart, O., Steffen, B.: Model-checking the full-modal mu-calculus for infinite sequential processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol.\u00a01256, pp. 419\u2013429. Springer, Heidelberg (1997)"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. Technical Report TUM-I0002, Technische Universit\u00e4t M\u00fcnchen, Department of Computer Science (February 2000)","DOI":"10.1007\/10722167_20"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-49019-1_2","volume-title":"Foundations of Software Science and Computation Structures","author":"J. Esparza","year":"1999","unstructured":"Esparza, J., Knoop, J.: An automata-theoretic approach to interprocedural data-flow analysis. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol.\u00a01578, pp. 14\u201330. Springer, Heidelberg (1999)"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Esparza, J., Podelski, A.: Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In: Proceedings of POPL 2000 (2000)","DOI":"10.1145\/325694.325697"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Electronic Notes in Theoretical Computer Science\u00a09 (1997)","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"20_CR8","unstructured":"Jensen, T., Le M\u00e9tayer, D., Thorn, T.: Verification of control flow based security properties. Technical Report 1210, IRISA (1998)"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-49727-7_22","volume-title":"Static Analysis","author":"D. Schmidt","year":"1998","unstructured":"Schmidt, D., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Levi, G. (ed.) SAS 1998. LNCS, vol.\u00a01503, pp. 351\u2013380. Springer, Heidelberg (1998)"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Tarjan, R.E.: Depth first search and linear graph algorithms. In: SICOMP, vol.\u00a01, pp. 146\u2013160 (1972)","DOI":"10.1137\/0201010"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"I. Walukiewicz","year":"1996","unstructured":"Walukiewicz, I.: Pushdown Processes: Games and Model Checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722167_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T07:48:46Z","timestamp":1556005726000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722167_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677703","9783540450474"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/10722167_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000]]}}}