{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:16:37Z","timestamp":1767928597754,"version":"3.49.0"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308222","type":"print"},{"value":"9783031308239","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially infinite domains. We present a framework that translates the reachability problem for such systems to the reachability problem for register machines enriched with the given abstract data type.<\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_30","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T20:19:12Z","timestamp":1682108352000},"page":"588-606","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Parameterized Verification under TSO with Data Types"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Mohamad Faouzi","family":"Atig","sequence":"additional","affiliation":[]},{"given":"Florian","family":"Furbach","sequence":"additional","affiliation":[]},{"given":"Adwait A.","family":"Godbole","sequence":"additional","affiliation":[]},{"given":"Yacoub G.","family":"Hendi","sequence":"additional","affiliation":[]},{"given":"Shankara N.","family":"Krishna","sequence":"additional","affiliation":[]},{"given":"Stephan","family":"Spengler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"30_CR1","doi-asserted-by":"crossref","unstructured":"Parosh\u00a0Aziz Abdulla.Regular model checking.STTT, 14(2):109\u2013118, 2012.","DOI":"10.1007\/s10009-011-0216-8"},{"key":"30_CR2","unstructured":"Parosh\u00a0Aziz Abdulla, Mohamed\u00a0Faouzi Atig, Ahmed Bouajjani, and Tuan\u00a0Phong Ngo. A load-buffer semantics for total store ordering.LMCS, 14(1), 2018."},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"Parosh\u00a0Aziz Abdulla, Mohamed\u00a0Faouzi Atig, Florian Furbach, Adwait Godbole, Yacoub\u00a0G. Hendi, Shankaranarayanan Krishna, and Stephan Spengler. Parameterized verification under tso with data types. arXiv e-prints, 2023. arXiv:2302.02163.","DOI":"10.1007\/978-3-031-30823-9_30"},{"key":"30_CR4","doi-asserted-by":"crossref","unstructured":"Parosh\u00a0Aziz Abdulla, Mohamed\u00a0Faouzi Atig, and Rojin Rezvan. Parameterized verification under tso is pspace-complete. Proc. ACM Program. Lang., 4(POPL), 2019.","DOI":"10.1145\/3371094"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"Parosh\u00a0Aziz Abdulla, Yu-Fang Chen, Giorgio Delzanno, Fr\u00e9d\u00e9ric Haziza, Chih-Duo Hong, and Ahmed Rezine. Constrained monotonic abstraction: A CEGAR for parameterized verification. In CONCUR 2010, pages 86\u2013101, 2010.","DOI":"10.1007\/978-3-642-15375-4_7"},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Parosh\u00a0Aziz Abdulla and Giorgio Delzanno. Parameterized verification. STTT, 18(5):469\u2013473, 2016.","DOI":"10.1007\/s10009-016-0424-3"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"Parosh\u00a0Aziz Abdulla, Fr\u00e9d\u00e9ric Haziza, and Luk\u00e1s Hol\u00edk. Parameterized verification through view abstraction. STTT, 18(5):495\u2013516, 2016.","DOI":"10.1007\/s10009-015-0406-x"},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"Parosh\u00a0Aziz Abdulla, A.\u00a0Prasad Sistla, and Muralidhar Talupur. Model checking parameterized systems. In Handbook of Model Checking, pages 685\u2013725. Springer, 2018.","DOI":"10.1007\/978-3-319-10575-8_21"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"Parosh\u00a0Aziz Abdulla, K\u0101rlis \u010cer\u0101ns, Bengt Jonsson, and Yih-Kuen Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput., 160:109\u2013127, 2000.","DOI":"10.1006\/inco.1999.2843"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"Krzysztof\u00a0R. Apt and Dexter Kozen. Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett., 22(6):307\u2013309, 1986.","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"30_CR11","doi-asserted-by":"crossref","unstructured":"Mohamed\u00a0Faouzi Atig. Model-Checking of Ordered Multi-Pushdown Automata. LMCS, Volume 8, Issue 3, 2012.","DOI":"10.2168\/LMCS-8(3:20)2012"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"Mohamed\u00a0Faouzi Atig, Benedikt Bollig, and Peter Habermehl. Emptiness of multi-pushdown automata is 2etime-complete. In Developments in Language Theory, pages 121\u2013133. Springer, 2008.","DOI":"10.1007\/978-3-540-85780-8_9"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. Decidability in parameterized verification. SIGACT News, 47(2):53\u201364, 2016.","DOI":"10.1145\/2951860.2951873"},{"key":"30_CR14","doi-asserted-by":"crossref","unstructured":"Bernard Boigelot, Axel Legay, and Pierre Wolper. Iterating transducers in the large (extended abstract). In CAV, volume 2725 of LNCS, pages 223\u2013235. Springer, 2003.","DOI":"10.1007\/978-3-540-45069-6_24"},{"key":"30_CR15","doi-asserted-by":"crossref","unstructured":"Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer. Checking and enforcing robustness against TSO. In ETAPS, pages 533\u2013553, 2013.","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"Ahmed Bouajjani, Peter Habermehl, Adam Rogalewicz, and Tom\u00e1s Vojnar. Abstract regular (tree) model checking. STTT, 14(2):167\u2013191, 2012.","DOI":"10.1007\/s10009-011-0205-y"},{"key":"30_CR17","doi-asserted-by":"crossref","unstructured":"Sebastian Burckhardt. Principles of eventual consistency. FTPL, 1(1-2):1\u2013150, 2014.","DOI":"10.1561\/2500000011"},{"key":"30_CR18","unstructured":"Thierry Cachat and Igor Walukiewicz. The complexity of games on higher order pushdown automata. CoRR, abs\/0705.0262, 2007."},{"key":"30_CR19","doi-asserted-by":"crossref","unstructured":"Sylvain Conchon, David Declerck, and Fatiha Za\u00efdi. Parameterized model checking on the tso weak memory model. J. Autom. Reason., 64(7):1307\u20131330, 2020.","DOI":"10.1007\/s10817-020-09565-w"},{"key":"30_CR20","doi-asserted-by":"crossref","unstructured":"Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. Parameterized verification of ad hoc networks. In CONCUR, pages 313\u2013327, 2010.","DOI":"10.1007\/978-3-642-15375-4_22"},{"key":"30_CR21","doi-asserted-by":"crossref","unstructured":"Marco Elver and Vijay Nagarajan. TSO-CC: consistency directed cache coherence for TSO. In HPCA, pages 165\u2013176. IEEE, 2014.","DOI":"10.1109\/HPCA.2014.6835927"},{"key":"30_CR22","doi-asserted-by":"crossref","unstructured":"E.\u00a0Allen Emerson, John Havlicek, and Richard\u00a0J. Trefler. Virtual symmetry reduction. In LICS, pages 121\u2013131, 2000.","DOI":"10.1109\/LICS.2000.855761"},{"key":"30_CR23","doi-asserted-by":"crossref","unstructured":"E.\u00a0Allen Emerson and Vineet Kahlon. Exact and efficient verification of parameterized cache coherence protocols. In CHARME, volume 2860 of LNCS, pages 247\u2013262. Springer, 2003.","DOI":"10.1007\/978-3-540-39724-3_22"},{"key":"30_CR24","doi-asserted-by":"crossref","unstructured":"E.\u00a0Allen Emerson and Vineet Kahlon. Parameterized model checking of ring-based message passing systems. In CSL, volume 3210 of LNCS, pages 325\u2013339. Springer, 2004.","DOI":"10.1007\/978-3-540-30124-0_26"},{"key":"30_CR25","doi-asserted-by":"crossref","unstructured":"Joost Engelfriet. Iterated stack automata and complexity classes.Inf. Comput., 95(1):21\u201375, 1991.","DOI":"10.1016\/0890-5401(91)90015-T"},{"key":"30_CR26","unstructured":"Javier Esparza. Decidability and complexity of petri net problems - an introduction.LNCS, 1491, 2000."},{"key":"30_CR27","doi-asserted-by":"crossref","unstructured":"Javier Esparza, Alain Finkel, and Richard Mayr. On the verification of broadcast protocols. In LICS, pages 352\u2013359. IEEE Computer Society, 1999.","DOI":"10.1109\/LICS.1999.782630"},{"key":"30_CR28","doi-asserted-by":"crossref","unstructured":"Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. J. ACM, 63(1):10:1\u201310:48, 2016.","DOI":"10.1145\/2842603"},{"key":"30_CR29","doi-asserted-by":"crossref","unstructured":"A.\u00a0Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1):63\u201392, 2001. ISS.","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"30_CR30","doi-asserted-by":"crossref","unstructured":"Marie Fortin, Anca Muscholl, and Igor Walukiewicz. Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems. In CAV, pages 155\u2013175, 2017.","DOI":"10.1007\/978-3-319-63390-9_9"},{"key":"30_CR31","doi-asserted-by":"crossref","unstructured":"Pierre Ganty and Rupak Majumdar. Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst., 34(1):6:1\u20136:48, 2012.","DOI":"10.1145\/2160910.2160915"},{"key":"30_CR32","doi-asserted-by":"crossref","unstructured":"Steven\u00a0M. German and A.\u00a0Prasad Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675\u2013735, 1992.","DOI":"10.1145\/146637.146681"},{"key":"30_CR33","unstructured":"Matthew Hague. Parameterised pushdown systems with non-atomic writes. In FSTTCS, pages 457\u2013468, 2011."},{"key":"30_CR34","doi-asserted-by":"crossref","unstructured":"Alexander Heu\u00dfner and Alexander Kartzow. Reachability in higher-order-counters. In MFCS, pages 528\u2013539. Springer, 2013.","DOI":"10.1007\/978-3-642-40313-2_47"},{"key":"30_CR35","doi-asserted-by":"crossref","unstructured":"Alexander Heu\u00dfner, J\u00e9r\u00f4me Leroux, Anca Muscholl, and Gr\u00e9goire Sutre.Reachability analysis of communicating pushdown systems. In FOSSACS, pages 267\u2013281. Springer, 2010.","DOI":"10.1007\/978-3-642-12032-9_19"},{"key":"30_CR36","doi-asserted-by":"crossref","unstructured":"Vineet Kahlon. Parameterization as abstraction: A tractable approach to the dataflow analysis of concurrent programs. In LICS, pages 181\u2013192, 2008.","DOI":"10.1109\/LICS.2008.37"},{"key":"30_CR37","doi-asserted-by":"crossref","unstructured":"Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Dynamic cutoff detection in parameterized concurrent programs. In CAV, volume 6174 of LNCS, pages 645\u2013659. Springer, 2010.","DOI":"10.1007\/978-3-642-14295-6_55"},{"key":"30_CR38","doi-asserted-by":"crossref","unstructured":"Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, and Elad Shahar. Symbolic model checking with rich assertional languages. Theor. Comput. Sci., 256(1-2):93\u2013112, 2001.","DOI":"10.1016\/S0304-3975(00)00103-1"},{"key":"30_CR39","doi-asserted-by":"crossref","unstructured":"Shankara\u00a0Narayanan Krishna, Adwait Godbole, Roland Meyer, and Soham Chakraborty. Parameterized verification under release acquire is pspace-complete.In PODC, pages 482\u2013492. ACM, 2022.","DOI":"10.1145\/3519270.3538445"},{"key":"30_CR40","unstructured":"Salvatore La Torre, Anca Muscholl, and Igor Walukiewicz. Safety of parametrized asynchronous shared-memory systems is almost always decidable. In CONCUR, pages 72\u201384, 2015."},{"key":"30_CR41","doi-asserted-by":"crossref","unstructured":"Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. Taming release-acquire consistency. In SIGPLAN-SIGACT, pages 649\u2013662. ACM, 2016.","DOI":"10.1145\/2914770.2837643"},{"key":"30_CR42","doi-asserted-by":"crossref","unstructured":"Anca Muscholl, Helmut Seidl, and Igor Walukiewicz. Reachability for dynamic parametric processes. In VMCAI, pages 424\u2013441, 2017.","DOI":"10.1007\/978-3-319-52234-0_23"},{"key":"30_CR43","doi-asserted-by":"crossref","unstructured":"Kedar\u00a0S. Namjoshi and Richard\u00a0J. Trefler. Parameterized compositional model checking. In ETAPS, volume 9636 of LNCS, pages 589\u2013606. Springer, 2016.","DOI":"10.1007\/978-3-662-49674-9_39"},{"key":"30_CR44","unstructured":"J.\u00a0L. Peterson. Petri Net Theory and the Modeling of Systems. Prentice Hall PTR, 1981."},{"key":"30_CR45","unstructured":"Ahmed\u00a0Bouajjani Rajeev\u00a0Alur and Javier Esparza. Handbook of Model Checking, chapter Model Checking Procedural Programs, pages 547\u2013569. Springer, 2018."},{"key":"30_CR46","unstructured":"Alberto Ros and Stefanos Kaxiras. Racer: TSO consistency via race detection. In MICRO, pages 33:1\u201333:13. IEEE Computer Society, 2016."},{"key":"30_CR47","doi-asserted-by":"crossref","unstructured":"Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. Understanding POWER multiprocessors. In ACM SIGPLAN, PLDI, pages 175\u2013186. ACM, 2011.","DOI":"10.1145\/1993316.1993520"},{"key":"30_CR48","doi-asserted-by":"crossref","unstructured":"Peter Sewell, Susmit Sarkar, Scott Owens, Francesco\u00a0Zappa Nardelli, and Magnus\u00a0O. Myreen. x86-tso: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM, 53(7):89\u201397, 2010.","DOI":"10.1145\/1785414.1785443"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,19]],"date-time":"2024-10-19T00:23:13Z","timestamp":1729297393000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"169","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"56","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}