{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:15:59Z","timestamp":1770282959857,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642385353","type":"print"},{"value":"9783642385360","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38536-0_35","type":"book-chapter","created":{"date-parts":[[2013,6,2]],"date-time":"2013-06-02T21:03:04Z","timestamp":1370206984000},"page":"405-417","source":"Crossref","is-referenced-by-count":7,"title":["Model-Checking Bounded Multi-Pushdown Systems"],"prefix":"10.1007","author":[{"given":"Kshitij","family":"Bansal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phane","family":"Demri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"35_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-540-24730-2_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Alur","year":"2004","unstructured":"Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 467\u2013481. Springer, Heidelberg (2004)"},{"key":"35_CR2","unstructured":"Atig, M.: Global model checking of ordered multi-pushdown systems. In: FST&TCS 2010. LIPICS, pp. 216\u2013227 (2010)"},{"key":"35_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-85780-8_9","volume-title":"Developments in Language Theory","author":"M.F. Atig","year":"2008","unstructured":"Atig, M.F., Bollig, B., Habermehl, P.: Emptiness of multi-pushdown automata is 2ETIME-complete. In: Ito, M., Toyama, M. (eds.) DLT 2008. LNCS, vol.\u00a05257, pp. 121\u2013133. Springer, Heidelberg (2008)"},{"key":"35_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-33386-6_13","volume-title":"Automated Technology for Verification and Analysis","author":"M.F. Atig","year":"2012","unstructured":"Atig, M.F., Bouajjani, A., Narayan Kumar, K., Saivasan, P.: Linear-time model-checking for multithreaded programs under scope-bounding. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 152\u2013166. Springer, Heidelberg (2012)"},{"key":"35_CR5","unstructured":"Bansal, K., Demri, S.: A note on the complexity of model-checking bounded multi-pushdown systems. Technical Report TR2012-949, NYU (December 2012)"},{"key":"35_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-22993-0_15","volume-title":"Mathematical Foundations of Computer Science 2011","author":"B. Bollig","year":"2011","unstructured":"Bollig, B., Cyriac, A., Gastin, P., Zeitoun, M.: Temporal logics for concurrent recursive programs: Satisfiability and model checking. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol.\u00a06907, pp. 132\u2013144. Springer, Heidelberg (2011)"},{"key":"35_CR7","doi-asserted-by":"crossref","unstructured":"Bollig, B., Kuske, D., Mennicke, R.: The complexity of model-checking multi-stack systems (2012) (submitted)","DOI":"10.1109\/LICS.2013.22"},{"key":"35_CR8","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":"35_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-642-32940-1_38","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"A. Cyriac","year":"2012","unstructured":"Cyriac, A., Gastin, P., Kumar, K.N.: MSO decidability of multi-pushdown systems via split-width. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol.\u00a07454, pp. 547\u2013561. Springer, Heidelberg (2012)"},{"key":"35_CR10","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ganty, P.: Complexity of pattern-based verification for multithreaded programs. In: POPL 2011, pp. 499\u2013510. ACM (2011)","DOI":"10.1145\/1925844.1926443"},{"key":"35_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/3-540-45500-0_16","volume-title":"Theoretical Aspects of Computer Software","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Ku\u010dera, A., Schwoon, S.: Model-checking LTL with regular valuations for pushdown systems. In: Kobayashi, N., Babu, C. S. (eds.) TACS 2001. LNCS, vol.\u00a02215, pp. 316\u2013339. Springer, Heidelberg (2001)"},{"key":"35_CR12","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS 2007, pp. 161\u2013170. IEEE (2007)","DOI":"10.1109\/LICS.2007.9"},{"key":"35_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-642-23217-6_14","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"S. La Torre","year":"2011","unstructured":"La Torre, S., Napoli, M.: Reachability of multistack pushdown systems with scope-bounded matching relations. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol.\u00a06901, pp. 203\u2013218. Springer, Heidelberg (2011)"},{"key":"35_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-33475-7_16","volume-title":"Theoretical Computer Science","author":"S. La Torre","year":"2012","unstructured":"La Torre, S., Napoli, M.: A temporal logic for multi-threaded programs. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol.\u00a07604, pp. 225\u2013239. Springer, Heidelberg (2012)"},{"key":"35_CR15","unstructured":"La Torre, S., Parlato, G.: Scope-bounded multistack pushdown systems: fixed-point, sequentialization and tree-width. In: FSTTCS 2012. LIPICS, pp. 173\u2013184 (2012)"},{"key":"35_CR16","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G.: The tree width of auxiliary storage. In: POPL 2011, pp. 283\u2013294. ACM (2011)","DOI":"10.1145\/1925844.1926419"},{"key":"35_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"key":"35_CR18","unstructured":"Schwoon, S.: Model-checking pushdown systems. PhD thesis, TUM (2002)"}],"container-title":["Lecture Notes in Computer Science","Computer Science \u2013 Theory and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38536-0_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T12:23:37Z","timestamp":1557750217000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38536-0_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385353","9783642385360"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38536-0_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}