{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T12:26:25Z","timestamp":1749644785512},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642401831"},{"type":"electronic","value":"9783642401848"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40184-8_21","type":"book-chapter","created":{"date-parts":[[2013,7,23]],"date-time":"2013-07-23T01:50:56Z","timestamp":1374544256000},"page":"288-302","source":"Crossref","is-referenced-by-count":4,"title":["Safety Verification of Asynchronous Pushdown Systems with Shaped Stacks"],"prefix":"10.1007","author":[{"given":"Jonathan","family":"Kochems","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C. -H. Luke","family":"Ong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"Babic, D., Rakamaric, Z.: Asynchronously communicating visibly pushdown systems. Technical Report UCB\/EECS-2011-108, UC Berkeley (2011)"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Emmi, M.: Analysis of recursively parallel programs. In: POPL, pp. 203\u2013214 (2012)","DOI":"10.1145\/2103621.2103681"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-642-28756-5_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Bouajjani","year":"2012","unstructured":"Bouajjani, A., Emmi, M.: Bounded phase analysis of message-passing programs. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 451\u2013465. Springer, Heidelberg (2012)"},{"key":"21_CR4","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":"21_CR5","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. ACM\u00a030(2), 323\u2013342 (1983)","journal-title":"J. ACM"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-540-74407-8_10","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"R. Chadha","year":"2007","unstructured":"Chadha, R., Viswanathan, M.: Decidability results for well-structured transition systems with auxiliary storage. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 136\u2013150. Springer, Heidelberg (2007)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-642-04081-8_18","volume-title":"CONCUR 2009 - Concurrency Theory","author":"W. Czerwi\u0144ski","year":"2009","unstructured":"Czerwi\u0144ski, W., Fr\u00f6schle, S., Lasota, S.: Partially-commutative context-free processes. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol.\u00a05710, pp. 259\u2013273. Springer, Heidelberg (2009)"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-32940-1_6","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"W. Czerwi\u0144ski","year":"2012","unstructured":"Czerwi\u0144ski, W., Hofman, P., Lasota, S.: Reachability problem for weak multi-pushdown automata. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol.\u00a07454, pp. 53\u201368. Springer, Heidelberg (2012)"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"D\u2019Osualdo, E., Kochems, J., Ong, C.-H.L.: Soter: an automatic safety verifier for Erlang. In: AGERE! 2012, pp. 137\u2013140 (2012)","DOI":"10.1145\/2414639.2414658"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"D\u2019Osualdo, E., Kochems, J., Ong, C.-H.L.: Automatic verification of Erlang-style concurrency. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol.\u00a07935, pp. 454\u2013476. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-38856-9_24"},{"issue":"1","key":"21_CR11","doi-asserted-by":"crossref","first-page":"13","DOI":"10.3233\/FI-1997-3112","volume":"31","author":"J. Esparza","year":"1997","unstructured":"Esparza, J.: Petri nets, commutative context-free grammars, and basic parallel processes. Fundam. Inform.\u00a031(1), 13\u201325 (1997)","journal-title":"Fundam. Inform."},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ganty, P.: Complexity of pattern-based verification for multithreaded programs. In: POPL, pp. 499\u2013510 (2011)","DOI":"10.1145\/1925844.1926443"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Esparza, J., Podelski, A.: Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In: POPL, pp. 1\u201311 (2000)","DOI":"10.1145\/325694.325697"},{"key":"21_CR14","unstructured":"Esparza, J., Ganty, P., Kiefer, S., Luttenberger, M.: Parikh\u2019s theorem: A simple and direct construction. CoRR, abs\/1006.3825 (2010)"},{"issue":"1-2","key":"21_CR15","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"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-44829-2_14","volume-title":"Model Checking Software","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 213\u2013224. Springer, Heidelberg (2003)"},{"issue":"1","key":"21_CR17","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/2160910.2160915","volume":"34","author":"P. Ganty","year":"2012","unstructured":"Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst.\u00a034(1), 6 (2012)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Ganty, P., Majumdar, R., Rybalchenko, A.: Verifying liveness for asynchronous programs. In: POPL, pp. 102\u2013113 (2009)","DOI":"10.1145\/1594834.1480895"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Geeraerts, G., Heu\u00dfner, A., Raskin, J.-F.: Queue-dispatch asynchronous systems. CoRR, abs\/1201.4871 (2012)","DOI":"10.1109\/ACSD.2013.18"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-540-45069-6_27","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Qadeer, S.: Thread-modular abstraction refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 262\u2013274. Springer, Heidelberg (2003)"},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-12032-9_19","volume-title":"Foundations of Software Science and Computational Structures","author":"A. Heu\u00dfner","year":"2010","unstructured":"Heu\u00dfner, A., Leroux, J., Muscholl, A., Sutre, G.: Reachability analysis of communicating pushdown systems. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol.\u00a06014, pp. 267\u2013281. Springer, Heidelberg (2010)"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Interprocedural analysis of asynchronous programs. In: POPL, pp. 339\u2013350 (2007)","DOI":"10.1145\/1190215.1190266"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Kahlon, V.: Boundedness vs. unboundedness of lock chains: Characterizing decidability of pairwise CFL-reachability for threads communicating via locks. In: LICS, pp. 27\u201336 (2009)","DOI":"10.1109\/LICS.2009.45"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Kochems, J., Ong, C.-H.L.: Safety verification of asynchronous pushdown systems with shaped stacks (long version) (2013), http:\/\/www.cs.ox.ac.uk\/people\/jonathan.kochems\/apcps.pdf","DOI":"10.1007\/978-3-642-40184-8_21"},{"issue":"1","key":"21_CR25","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10703-009-0078-9","volume":"35","author":"A. Lal","year":"2009","unstructured":"Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods in System Design\u00a035(1), 73\u201397 (2009)","journal-title":"Formal Methods in System Design"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"Long, Z., Calin, G., Majumdar, R., Meyer, R.: Language-theoretic abstraction refinement. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol.\u00a07212, pp. 362\u2013376. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28872-2_25"},{"key":"21_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/3-540-49366-2_21","volume-title":"Advances in Computing Science - ASIAN\u201998","author":"M. Mukund","year":"1998","unstructured":"Mukund, M., Narayan Kumar, K., Radhakrishnan, J., Sohoni, M.: Towards a characterisation of finite-state message-passing systems. In: Hsiang, J., Ohori, A. (eds.) ASIAN 1998. LNCS, vol.\u00a01538, pp. 282\u2013299. Springer, Heidelberg (1998)"},{"key":"21_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/BFb0055052","volume-title":"Automata, Languages and Programming","author":"M. Mukund","year":"1998","unstructured":"Mukund, M., Narayan Kumar, K., Radhakrishnan, J., Sohoni, M.: Robust asynchronous protocols are finite-state. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 188\u2013199. Springer, Heidelberg (1998)"},{"issue":"2","key":"21_CR29","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G. Ramalingam","year":"2000","unstructured":"Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst.\u00a022(2), 416\u2013430 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"21_CR30","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 asynchronous atomic methods. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 300\u2013314. Springer, Heidelberg (2006)"},{"key":"21_CR31","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. Torre La","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":"21_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-642-02658-4_36","volume-title":"Computer Aided Verification","author":"S. Torre La","year":"2009","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Reducing context-bounded concurrent reachability to sequential reachability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 477\u2013492. Springer, Heidelberg (2009)"},{"key":"21_CR33","unstructured":"Wehrman, I.: Higman\u2019s theorem and the multiset order (2006), http:\/\/www.cs.utexas.edu\/~iwehrman\/pub\/ms-wqo.pdf"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2013 \u2013 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40184-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,31]],"date-time":"2020-07-31T12:31:51Z","timestamp":1596198711000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40184-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642401831","9783642401848"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40184-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}