{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:17Z","timestamp":1784793797158,"version":"3.55.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    This paper investigates the algorithmic safety verification problem of infinite-state parameterized concurrent programs over a rich set of communication topologies. The goal is to automatically produce a proof of correctness in the form of a\n                    <jats:italic>universally quantified<\/jats:italic>\n                    inductive invariant, where the quantification is over the nodes in the topology. We illustrate that under reasonable assumptions on the underlying topology, the problem can be reduced to and solved as a\n                    <jats:italic>compositional<\/jats:italic>\n                    scheme, that is, the verification of the parameterized family is reduced to a set of\n                    <jats:italic>local<\/jats:italic>\n                    proofs, in a\n                    <jats:italic>complete<\/jats:italic>\n                    manner. We propose a verification algorithm and demonstrate through a set of benchmarks over several different topologies that our approach is effective in proving parameterized programs safe.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_4","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:40Z","timestamp":1784791060000},"page":"67-89","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Complete Local Reasoning About Parameterized Programs Over Topologies"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-1857-7251","authenticated-orcid":false,"given":"Ruotong","family":"Cheng","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9005-2653","authenticated-orcid":false,"given":"Azadeh","family":"Farzan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"issue":"5","key":"4_CR1","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/s10009-016-0424-3","volume":"18","author":"PA Abdulla","year":"2016","unstructured":"Abdulla, P.A., Delzanno, G.: Parameterized verification. Int. J. Softw. Tools Technol. Transfer 18(5), 469\u2013473 (2016). https:\/\/doi.org\/10.1007\/s10009-016-0424-3","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: All for the price of few. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 476\u2013495. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_28","DOI":"10.1007\/978-3-642-35873-9_28"},{"issue":"3","key":"4_CR3","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/s00446-017-0302-6","volume":"31","author":"B Aminof","year":"2018","unstructured":"Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. Distrib. Comput. 31(3), 187\u2013222 (2018). https:\/\/doi.org\/10.1007\/s00446-017-0302-6","journal-title":"Distrib. Comput."},{"issue":"6","key":"4_CR4","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986). https:\/\/doi.org\/10.1016\/0020-0190(86)90071-2","journal-title":"Inf. Process. Lett."},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-030-20652-9_3","volume-title":"NASA Formal Methods","author":"R Ashmore","year":"2019","unstructured":"Ashmore, R., Gurfinkel, A., Trefler, R.: Local Reasoning for Parameterized First Order Protocols. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2019. LNCS, vol. 11460, pp. 36\u201353. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_3"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Blicha, M., Britikov, K., Sharygina, N.: The Golem Horn Solver. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, pp. 209\u2013223. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_10","DOI":"10.1007\/978-3-031-37703-7_10"},{"key":"4_CR7","doi-asserted-by":"publisher","unstructured":"Cheng, R., Farzan, A.: Complete Local Reasoning About Parameterized Programs Over Topologies (2026). https:\/\/doi.org\/10.48550\/arXiv.2605.15143","DOI":"10.48550\/arXiv.2605.15143"},{"key":"4_CR8","doi-asserted-by":"publisher","DOI":"10.5281\/ZENODO.19851981","author":"R Cheng","year":"2026","unstructured":"Cheng, R., Farzan, A.: Mosaic: artifact for \u201ccomplete local reasoning about parameterized programs over topologies\u2019\u2019. Zenodo (2026). https:\/\/doi.org\/10.5281\/ZENODO.19851981","journal-title":"Zenodo"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Cheng, R., Farzan, A.: Symmetric Proofs of Parameterized Programs (2026). https:\/\/doi.org\/10.48550\/arXiv.2601.18745","DOI":"10.48550\/arXiv.2601.18745"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 85\u201394. POPL \u201995, Association for Computing Machinery, New York, NY, USA (1995). https:\/\/doi.org\/10.1145\/199448.199468","DOI":"10.1145\/199448.199468"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Emmi, M., Majumdar, R., Manevich, R.: Parameterized verification of transactional memories. In: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 134\u2013145. PLDI \u201910, Association for Computing Machinery, New York, NY, USA (2010). https:\/\/doi.org\/10.1145\/1806596.1806613","DOI":"10.1145\/1806596.1806613"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Proof spaces for unbounded parallelism. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 407\u2013420. ACM, Mumbai India (2015). https:\/\/doi.org\/10.1145\/2676726.2677012","DOI":"10.1145\/2676726.2677012"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Farzan, A., Klumpp, D., Podelski, A.: Commutativity Simplifies Proofs of Parameterized Programs. Proc. ACM Program. Lang. 8(POPL), 2485\u20132513 (2024). https:\/\/doi.org\/10.1145\/3632925","DOI":"10.1145\/3632925"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Shoham, S., Meshman, Y.: SMT-based verification of parameterized systems. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 338\u2013348. FSE 2016, Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2950290.2950330","DOI":"10.1145\/2950290.2950330"},{"key":"4_CR16","volume-title":"A Shorter Model Theory","author":"W Hodges","year":"1997","unstructured":"Hodges, W.: A Shorter Model Theory. Cambridge University Press, Cambridge; New York (1997)"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Hoenicke, J., Majumdar, R., Podelski, A.: Thread modularity at many levels: A pearl in compositional verification. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 473\u2013485. ACM, Paris, France (2017). https:\/\/doi.org\/10.1145\/3009837.3009893","DOI":"10.1145\/3009837.3009893"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Hojjat, H., R\u00fcmmer, P.: The ELDARICA Horn Solver. Formal Methods in Computer Aided Design (FMCAD), pp. 1\u20137 (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"4_CR19","doi-asserted-by":"publisher","first-page":"39","DOI":"10.4204\/EPTCS.169.6","volume":"169","author":"H Hojjat","year":"2014","unstructured":"Hojjat, H., R\u00fcmmer, P., Subotic, P., Yi, W.: Horn clauses for communicating timed systems. EPTCS 169, 39\u201352 (2014)","journal-title":"EPTCS"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Koenig, J.R., Padon, O., Immerman, N., Aiken, A.: First-order quantified separators. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 703\u2013717. ACM Conferences, Association for Computing Machinery (2020). https:\/\/doi.org\/10.1145\/3385412.3386018","DOI":"10.1145\/3385412.3386018"},{"issue":"3","key":"4_CR21","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175\u2013205 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0249-4","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Libkin, L.: Elements of Finite Model Theory. Springer Berlin Heidelberg, Berlin, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-07003-1","DOI":"10.1007\/978-3-662-07003-1"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-662-53413-7_18","volume-title":"Static Analysis","author":"D Monniaux","year":"2016","unstructured":"Monniaux, D., Gonnord, L.: Cell Morphing: From Array Programs to Array-Free Horn Clauses. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 361\u2013382. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53413-7_18"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-69738-1_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"KS Namjoshi","year":"2007","unstructured":"Namjoshi, K.S.: Symmetry and Completeness in the Analysis of Parameterized Systems. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 299\u2013313. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69738-1_22"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-27940-9_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"KS Namjoshi","year":"2012","unstructured":"Namjoshi, K.S., Trefler, R.J.: Local Symmetry and Compositional Verification. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 348\u2013362. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27940-9_23"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/978-3-662-49674-9_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KS Namjoshi","year":"2016","unstructured":"Namjoshi, K.S., Trefler, R.J.: Parameterized Compositional Model Checking. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 589\u2013606. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_39"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-319-89963-3_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KS Namjoshi","year":"2018","unstructured":"Namjoshi, K.S., Trefler, R.J.: Symmetry Reduction for the Local Mu-Calculus. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 379\u2013395. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_22"},{"issue":"6","key":"4_CR28","doi-asserted-by":"publisher","first-page":"614","DOI":"10.1145\/2980983.2908118","volume":"51","author":"O Padon","year":"2016","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. ACM SIGPLAN Notices 51(6), 614\u2013630 (2016). https:\/\/doi.org\/10.1145\/2980983.2908118","journal-title":"ACM SIGPLAN Notices"}],"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-032-32519-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:41Z","timestamp":1784791061000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Nothing relevant to declare.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"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":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}