{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:37:14Z","timestamp":1759639034127},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540304951"},{"type":"electronic","value":"9783540324195"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11590156_28","type":"book-chapter","created":{"date-parts":[[2005,12,5]],"date-time":"2005-12-05T10:43:16Z","timestamp":1133779396000},"page":"348-359","source":"Crossref","is-referenced-by-count":42,"title":["Reachability Analysis of Multithreaded Software with Asynchronous Communication"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[]},{"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Schwoon","sequence":"additional","affiliation":[]},{"given":"Jan","family":"Strej\u010dek","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_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)"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Schwoon, S., Strej\u010dek, J.: Reachability analysis of multithreaded software with asynchronous communication. Technical Report 2005\/06, Universit\u00e4t Stuttgart (2005) (a full version of this paper)","DOI":"10.1007\/11590156_28"},{"key":"28_CR3","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/604131.604137","volume-title":"Proceedings of POPL 2003","author":"A. Bouajjani","year":"2003","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: Proceedings of POPL 2003, pp. 62\u201373. ACM Press, New York (2003)"},{"key":"28_CR4","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: Reachability analysis of synchronized PA-systems. In: Proceedings of Infinity 2004 (2004) (to appear)"},{"key":"28_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 processes. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 473\u2013487. Springer, Heidelberg (2005)"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 232\u2013247. Springer, Heidelberg (2000)"},{"key":"28_CR7","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":"28_CR8","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G. Ramalingam","year":"2000","unstructured":"Ramalingam, G.: Context-sensitive synchronisation-sensitive analysis is undecidable. ACM Transactions on Programming Languages and Systems\u00a022, 416\u2013430 (2000)","journal-title":"ACM Transactions on Programming Languages and Systems"}],"container-title":["Lecture Notes in Computer Science","FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11590156_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T02:49:10Z","timestamp":1619491750000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11590156_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540304951","9783540324195"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/11590156_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}