{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:55Z","timestamp":1751660515262,"version":"3.41.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319633893"},{"type":"electronic","value":"9783319633909"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63390-9_9","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:50Z","timestamp":1499849630000},"page":"155-175","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems"],"prefix":"10.1007","author":[{"given":"Marie","family":"Fortin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anca","family":"Muscholl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Igor","family":"Walukiewicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"issue":"4","key":"9_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-7(4:4)2011","volume":"7","author":"MF Atig","year":"2011","unstructured":"Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. Log. Methods Comput. Sci. 7(4), 1\u201348 (2011)","journal-title":"Log. Methods Comput. Sci."},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/3-540-45319-9_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Ball","year":"2001","unstructured":"Ball, T., Chaki, S., Rajamani, S.K.: Parameterized verification of multithreaded software libraries. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 158\u2013173. Springer, Heidelberg (2001). doi:10.1007\/3-540-45319-9_12"},{"key":"9_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-02011-7","volume-title":"Decidability of Parameterized Verification","author":"R Bloem","year":"2015","unstructured":"Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Morgan & Claypool Publishers, San Rafael (2015)"},{"key":"9_CR4","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 1997: 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. 1243, pp. 135\u2013150. Springer, Heidelberg (1997). doi:10.1007\/3-540-63141-0_10"},{"key":"9_CR5","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., Strej\u0109ek, J.: Reachability analysis of multithreaded software with asynchronous communication. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 348\u2013359. Springer, Heidelberg (2005). doi:10.1007\/11590156_28"},{"key":"9_CR6","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., Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 473\u2013487. Springer, Heidelberg (2005). doi:10.1007\/11539452_36"},{"key":"9_CR7","unstructured":"Bouyer, P., Markey, N., Randour, M., Sangnier, A., Stan, D.: Reachability in networks of register protocols under stochastic schedulers. In: ICALP 2016, LIPIcs, pp. 106:1\u2013106:14. Leibniz-Zentrum f\u00fcr Informatik (2016)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/978-3-642-28756-5_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Chadha","year":"2012","unstructured":"Chadha, R., Madhusudan, P., Viswanathan, M.: Reachability under contextual locking. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 437\u2013450. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-28756-5_30"},{"issue":"5","key":"9_CR9","doi-asserted-by":"publisher","first-page":"726","DOI":"10.1145\/265943.265960","volume":"19","author":"EM Clarke","year":"1997","unstructured":"Clarke, E.M., Grumberg, O., Jha, S.: Verifying parameterized networks. ACM Trans. Program. Lang. Syst. 19(5), 726\u2013750 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9_CR10","first-page":"178","volume":"44","author":"B Courcelle","year":"1991","unstructured":"Courcelle, B.: On constructing obstruction sets of words. Bull. EATCS 44, 178\u2013186 (1991)","journal-title":"Bull. EATCS"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-09108-2_1","volume-title":"Graph Transformation","author":"G Delzanno","year":"2014","unstructured":"Delzanno, G.: Parameterized verification and model checking for distributed broadcast protocols. In: Giese, H., K\u00f6nig, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 1\u201316. Springer, Cham (2014). doi:10.1007\/978-3-319-09108-2_1"},{"issue":"2\u20133","key":"9_CR12","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/s10703-016-0258-3","volume":"50","author":"A Durand-Gasselin","year":"2017","unstructured":"Durand-Gasselin, A., Esparza, J., Ganty, P., Majumdar, R.: Model checking parameterized asynchronous shared-memory systems. Form. Methods Syst. Des. 50(2\u20133), 140\u2013167 (2017). Journal version of CAV 2015","journal-title":"Form. Methods Syst. Des."},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Model checking guarded protocols. In: LICS 2003, pp. 361\u2013370 (2003)","DOI":"10.1109\/LICS.2003.1210076"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS 1999, pp. 352\u2013359. IEEE (1999)","DOI":"10.1109\/LICS.1999.782630"},{"issue":"1","key":"9_CR15","doi-asserted-by":"publisher","first-page":"10:1","DOI":"10.1145\/2842603","volume":"63","author":"J Esparza","year":"2016","unstructured":"Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. J. ACM 63(1), 10:1\u201310:48 (2016). Journal version of CAV 2013","journal-title":"J. ACM"},{"issue":"6","key":"9_CR16","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/S0020-0190(00)00113-7","volume":"75","author":"K Etessami","year":"2000","unstructured":"Etessami, K.: A note on a question of Peled and Wilke regarding stutter-invariant LTL. Inf. Process. Lett. 75(6), 261\u2013263 (2000)","journal-title":"Inf. Process. Lett."},{"key":"9_CR17","unstructured":"Fortin, M., Muscholl, A., Walukiewicz, I.: On parametrized verification of asynchronous, shared-memory pushdown systems. CoRR, abs\/1606.08707 (2016)"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/3-540-13331-3_48","volume-title":"Logic and Machines: Decision Problems and Complexity","author":"M F\u00fcrer","year":"1984","unstructured":"F\u00fcrer, M.: The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems). In: B\u00f6rger, E., Hasenjaeger, G., R\u00f6dding, D. (eds.) LaM 1983. LNCS, vol. 171, pp. 312\u2013319. Springer, Heidelberg (1984). doi:10.1007\/3-540-13331-3_48"},{"issue":"3","key":"9_CR19","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"SA German","year":"1992","unstructured":"German, S.A., Sistla, P.A.: Reasoning about systems with many processes. J. ACM 39(3), 675\u2013735 (1992)","journal-title":"J. ACM"},{"key":"9_CR20","unstructured":"Hague, M.: Parameterised pushdown systems with non-atomic writes. In: FSTTCS 2011. LIPIcs, pp. 457\u2013468. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2011)"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Kahlon, V.: Parameterization as abstraction: a tractable approach to the dataflow analysis of concurrent programs. In: LICS 2008, pp. 181\u2013192. IEEE (2008)","DOI":"10.1109\/LICS.2008.37"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/11513988_49","volume-title":"Computer Aided Verification","author":"V Kahlon","year":"2005","unstructured":"Kahlon, V., Ivan\u010di\u0107, F., Gupta, A.: Reasoning about threads communicating via locks. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 505\u2013518. Springer, Heidelberg (2005). doi:10.1007\/11513988_49"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/978-3-642-14295-6_55","volume-title":"Computer Aided Verification","author":"A Kaiser","year":"2010","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 645\u2013659. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14295-6_55"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-45694-5_8","volume-title":"CONCUR 2002 \u2014 Concurrency Theory","author":"Y Kesten","year":"2002","unstructured":"Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.: Network invariants in action*. In: Brim, L., K\u0159et\u00ednsk\u00fd, M., Ku\u010dera, A., Jan\u010dar, P. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 101\u2013115. Springer, Heidelberg (2002). doi:10.1007\/3-540-45694-5_8"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1007\/978-3-642-14295-6_54","volume-title":"Computer Aided Verification","author":"S La Torre","year":"2010","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Model-checking parameterized concurrent programs using linear interfaces. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 629\u2013644. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14295-6_54"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Sequentializing parameterized programs. In: FIT 2012. EPTCS, vol. 87, pp. 34\u201347 (2012)","DOI":"10.4204\/EPTCS.87.4"},{"key":"9_CR27","unstructured":"La Torre, S., Muscholl, A., Walukiewicz, I.: Safety of parametrized asynchronous shared-memory systems is almost always decidable. In: CONCUR 2015. LIPIcs, vol. 42, pp. 72\u201384. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2015)"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-540-69166-2_14","volume-title":"Static Analysis","author":"P Lammich","year":"2008","unstructured":"Lammich, P., M\u00fcller-Olm, M.: Conflict analysis of programs with procedures, dynamic thread creation, and monitors. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 205\u2013220. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-69166-2_14"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-642-38856-9_25","volume-title":"Static Analysis","author":"P Lammich","year":"2013","unstructured":"Lammich, P., M\u00fcller-Olm, M., Seidl, H., Wenner, A.: Contextual locking for dynamic pushdown networks. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 477\u2013498. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-38856-9_25"},{"key":"9_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/978-3-642-02658-4_39","volume-title":"Computer Aided Verification","author":"P Lammich","year":"2009","unstructured":"Lammich, P., M\u00fcller-Olm, M., Wenner, A.: Predecessor sets of dynamic pushdown networks with tree-regular constraints. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 525\u2013539. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-02658-4_39"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-41540-6_7","volume-title":"Computer Aided Verification","author":"AW Lin","year":"2016","unstructured":"Lin, A.W., R\u00fcmmer, P.: Liveness of randomised parameterised systems under arbitrary schedulers. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 112\u2013133. Springer, Cham (2016). doi:10.1007\/978-3-319-41540-6_7"},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-319-52234-0_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Muscholl","year":"2017","unstructured":"Muscholl, A., Seidl, H., Walukiewicz, I.: Reachability for dynamic parametric processes. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 424\u2013441. Springer, Cham (2017). doi:10.1007\/978-3-319-52234-0_23"},{"key":"9_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-662-46681-0_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KS Namjoshi","year":"2015","unstructured":"Namjoshi, K.S., Trefler, R.J.: Analysis of dynamic process networks. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 164\u2013178. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46681-0_11"},{"issue":"5","key":"9_CR34","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/S0020-0190(97)00133-6","volume":"63","author":"DA Peled","year":"1997","unstructured":"Peled, D.A., Wilke, T.: Stutter-invariant temporal properties are expressible without the next-time operator. Inf. Process. Lett. 63(5), 243\u2013246 (1997)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"9_CR35","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. (TOPLAS) 22(2), 416\u2013430 (2000)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63390-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T01:07:09Z","timestamp":1750554429000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63390-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633893","9783319633909"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63390-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}