{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T13:21:45Z","timestamp":1770297705473,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642120312","type":"print"},{"value":"9783642120329","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12032-9_19","type":"book-chapter","created":{"date-parts":[[2010,3,7]],"date-time":"2010-03-07T20:07:56Z","timestamp":1267992476000},"page":"267-281","source":"Crossref","is-referenced-by-count":14,"title":["Reachability Analysis of Communicating Pushdown Systems"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Heu\u00dfner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00e9r\u00f4me","family":"Leroux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anca","family":"Muscholl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gr\u00e9goire","family":"Sutre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","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., Bouajjani, A., 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":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-540-85361-9_29","volume-title":"CONCUR 2008 - Concurrency Theory","author":"M.F. Atig","year":"2008","unstructured":"Atig, M.F., Bouajjani, A., Touili, T.: On the reachability analysis of acyclic networks of pushdown systems. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol.\u00a05201, pp. 356\u2013371. Springer, Heidelberg (2008)"},{"issue":"2","key":"19_CR3","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Inf. Comput.\u00a0127(2), 91\u2013101 (1996)","journal-title":"Inf. Comput."},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/11590156_28","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., Esparza, J., Schwoon, S., Strejcek, J.: Reachability analysis of multithreaded software with asynchronous communication. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol.\u00a03821, pp. 348\u2013359. Springer, Heidelberg (2005)"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/11539452_36","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., M\u00fcller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 473\u2013487. Springer, Heidelberg (2005)"},{"issue":"2","key":"19_CR6","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D. Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. of the ACM\u00a030(2), 323\u2013342 (1983)","journal-title":"J. of the ACM"},{"issue":"2","key":"19_CR7","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1016\/j.ic.2005.05.006","volume":"202","author":"G. C\u00e9c\u00e9","year":"2005","unstructured":"C\u00e9c\u00e9, G., Finkel, A.: Verification of programs with half-duplex communication. Inf. Comput.\u00a0202(2), 166\u2013190 (2005)","journal-title":"Inf. Comput."},{"issue":"2","key":"19_CR8","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1016\/S0890-5401(03)00139-1","volume":"186","author":"J. Esparza","year":"2003","unstructured":"Esparza, J., Kucera, A., Schwoon, S.: Model checking LTL with regular valuations for pushdown systems. Inf. Comput.\u00a0186(2), 355\u2013376 (2003)","journal-title":"Inf. Comput."},{"issue":"1-2","key":"19_CR9","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science\u00a0256(1-2), 63\u201392 (2001)","journal-title":"Theoretical Computer Science"},{"issue":"6","key":"19_CR10","doi-asserted-by":"publisher","first-page":"920","DOI":"10.1016\/j.ic.2006.01.005","volume":"204","author":"B. Genest","year":"2006","unstructured":"Genest, B., Kuske, D., Muscholl, A.: A Kleene theorem and model checking algorithms for existentially bounded communicating automata. Inf. Comput.\u00a0204(6), 920\u2013956 (2006)","journal-title":"Inf. Comput."},{"key":"19_CR11","first-page":"147","volume":"80","author":"B. Genest","year":"2007","unstructured":"Genest, B., Kuske, D., Muscholl, A.: On communicating automata with bounded channels. Fundamenta Informaticae\u00a080, 147\u2013167 (2007)","journal-title":"Fundamenta Informaticae"},{"key":"19_CR12","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1145\/1190216.1190266","volume-title":"POPL 2007","author":"R. Jhala","year":"2007","unstructured":"Jhala, R., Majumdar, R.: Interprocedural analysis of asynchronous programs. In: POPL 2007, pp. 339\u2013350. ACM, New York (2007)"},{"key":"19_CR13","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1145\/800070.802201","volume-title":"STOC 1982","author":"S. Rao Kosaraju","year":"1982","unstructured":"Rao Kosaraju, S.: Decidability of reachability in vector addition systems. In: STOC 1982, pp. 267\u2013281. ACM, New York (1982)"},{"issue":"2","key":"19_CR14","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/j.ic.2003.10.002","volume":"189","author":"M. Lohrey","year":"2004","unstructured":"Lohrey, M., Muscholl, A.: Bounded MSC communication. Inf. Comput.\u00a0189(2), 160\u2013181 (2004)","journal-title":"Inf. Comput."},{"key":"19_CR15","first-page":"161","volume-title":"LICS 2007","author":"S. Torre La","year":"2007","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS 2007, pp. 161\u2013170. IEEE, Los Alamitos (2007)"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-78800-3_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Torre La","year":"2008","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Context-bounded analysis of concurrent queue systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 299\u2013314. Springer, Heidelberg (2008)"},{"issue":"3","key":"19_CR17","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1137\/0213029","volume":"13","author":"E.W. Mayr","year":"1984","unstructured":"Mayr, E.W.: An algorithm for the general Petri net reachability problem. SIAM J. Comput.\u00a013(3), 441\u2013460 (1984)","journal-title":"SIAM J. Comput."},{"key":"19_CR18","volume-title":"Computational Complexity","author":"C. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.: Computational Complexity. Addison Wesley, Reading (1994)"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/11817963_29","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2006","unstructured":"Sen, K., Viswanathan, M.: Model checking multithreaded programs with synchronous atomic methods. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 300\u2013314. Springer, Heidelberg (2006)"}],"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-12032-9_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:47:00Z","timestamp":1606168020000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12032-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642120312","9783642120329"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12032-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}