{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:28:15Z","timestamp":1767929295077,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540853602","type":"print"},{"value":"9783540853619","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-85361-9_29","type":"book-chapter","created":{"date-parts":[[2008,8,18]],"date-time":"2008-08-18T12:28:04Z","timestamp":1219062484000},"page":"356-371","source":"Crossref","is-referenced-by-count":29,"title":["On the Reachability Analysis of Acyclic Networks of Pushdown Systems"],"prefix":"10.1007","author":[{"given":"Mohamed Faouzi","family":"Atig","sequence":"first","affiliation":[]},{"given":"Ahmed","family":"Bouajjani","sequence":"additional","affiliation":[]},{"given":"Tayssir","family":"Touili","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS 1996, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"issue":"1","key":"29_CR2","first-page":"39","volume":"25","author":"P.A. Abdulla","year":"2004","unstructured":"Abdulla, P.A., Collomb-Annichini, A., Bouajjani, A., Jonsson, B.: Using forward reachability analysis for verification of lossy channel systems. FMSD\u00a025(1), 39\u201365 (2004)","journal-title":"FMSD"},{"issue":"2","key":"29_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":"29_CR4","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Touili, T.: On the reachability analysis of acyclic networks of pushdown systems. Research report, LIAFA lab (April 2008)","DOI":"10.1007\/978-3-540-85361-9_29"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"Berstel, J.: Transductions and context-free langages. TeubnerStudienbucher Informatik (1979)","DOI":"10.1007\/978-3-663-09367-1"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol.\u00a03821, Springer, Heidelberg (2005)"},{"issue":"4","key":"29_CR7","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1142\/S0129054103001893","volume":"14","author":"A. Bouajjani","year":"2003","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. Int. J. Found. Comput. Sci.\u00a014(4), 551 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"29_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. Springer, Heidelberg (2005)"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1007\/978-3-540-24597-1_7","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"A. Bouajjani","year":"2003","unstructured":"Bouajjani, A., Touili, T.: Reachability analysis of process rewrite systems. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 74\u201387. Springer, Heidelberg (2003)"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Term Rewriting and Applications","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., Touili, T.: On computing reachability sets of process rewrite systems. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, Springer, Heidelberg (2005)"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/11805618_11","volume-title":"Term Rewriting and Applications","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Esparza, J.: Rewriting models of boolean programs. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 136\u2013150. Springer, Heidelberg (2006)"},{"key":"29_CR12","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":"29_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/11691372_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Chaki","year":"2006","unstructured":"Chaki, S., Clarke, E.M., Kidd, N., Reps, T.W., Touili, T.: Verifying concurrent message-passing c programs with recursive calls. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 334\u2013349. Springer, Heidelberg (2006)"},{"key":"29_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-77050-3_22","volume-title":"FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science","author":"P. Chambard","year":"2007","unstructured":"Chambard, P., Schnoebelen, P.: Post embedding problem is not primitive recursive, with applications to channel systems. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol.\u00a04855, pp. 265\u2013276. Springer, Heidelberg (2007)"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 dataflow analysis. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol.\u00a01578. Springer, Heidelberg (1999)"},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"Esparza, J., Podelski, A.: Efficient algorithms for pre $^{\\mbox{*}}$ and post $^{\\mbox{*}}$ on interprocedural parallel flow graphs. In: POPL, pp. 1\u201311 (2000)","DOI":"10.1145\/325694.325697"},{"issue":"1-2","key":"29_CR17","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! TCS\u00a0256(1-2), 63\u201392 (2001)","journal-title":"TCS"},{"key":"29_CR18","volume-title":"POPL","author":"R. Jhala","year":"2007","unstructured":"Jhala, R., Majumdar, R.: Interprocedural analysis of asynchronous programs. In: POPL. IEEE, Los Alamitos (2007)"},{"key":"29_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"V. Kahlon","year":"2005","unstructured":"Kahlon, V., Ivancic, F., Gupta, A.: Reasoning about threads communicating via locks. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576. Springer, Heidelberg (2005)"},{"key":"29_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. Springer, Heidelberg (2008)"},{"key":"29_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_20","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"P. Lammich","year":"2007","unstructured":"Lammich, P., M\u00fcller-Olm, M.: Precise fixpoint-based analysis of programs with thread-creation and procedures. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703. Springer, Heidelberg (2007)"},{"key":"29_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/BFb0055615","volume-title":"CONCUR \u201998 Concurrency Theory","author":"D. Lugiez","year":"1998","unstructured":"Lugiez, D., Schnoebelen, P.: The regular viewpoint on PA-processes. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 50\u201366. Springer, Heidelberg (1998)"},{"key":"29_CR23","doi-asserted-by":"crossref","unstructured":"Mayr, R.: Undecidable problems in unreliable computations. Theor. Comput. Sci.\u00a01-3(297) (2003)","DOI":"10.1016\/S0304-3975(02)00646-1"},{"key":"29_CR24","series-title":"Lecture Notes in Computer Science","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. Springer, Heidelberg (2005)"},{"key":"29_CR25","doi-asserted-by":"crossref","unstructured":"Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett. 83(5) (2002)","DOI":"10.1016\/S0020-0190(01)00337-4"},{"key":"29_CR26","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2002)"},{"key":"29_CR27","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":"29_CR28","first-page":"161","volume-title":"LICS","author":"S. Torre La","year":"2007","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS, pp. 161\u2013170. IEEE, Los Alamitos (2007)"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2008 - Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-85361-9_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T15:15:22Z","timestamp":1738336522000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-85361-9_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540853602","9783540853619"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-85361-9_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}