{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T20:46:15Z","timestamp":1770756375465,"version":"3.50.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032111753","type":"print"},{"value":"9783032111760","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-11176-0_8","type":"book-chapter","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T20:11:28Z","timestamp":1763842288000},"page":"106-123","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verification of\u00a0the\u00a0Release-Acquire Semantics"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6832-6611","authenticated-orcid":false,"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7526-9256","authenticated-orcid":false,"given":"Elli","family":"Anastasiadi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8229-3481","authenticated-orcid":false,"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0004-1762-8061","authenticated-orcid":false,"given":"Samuel","family":"Grahn","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,23]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Anastasiadi, E., Atig, M.F., Grahn, S.: Verification of the release-acquire semantics. arXiv entry (2025)","DOI":"10.1007\/978-3-032-11176-0_8"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Ngo, T.P.: Optimal stateless model checking under the release-acquire semantics. Proc. ACM Program. Lang. 2(OOPSLA), 135:1\u2013135:29 (2018)","DOI":"10.1145\/3276505"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, 27\u201330 July 1996, pp. 313\u2013321. IEEE Computer Society (1996)","DOI":"10.1109\/LICS.1996.561359"},{"issue":"1","key":"8_CR4","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/BF01784241","volume":"9","author":"M Ahamad","year":"1995","unstructured":"Ahamad, M., Neiger, G., Burns, J.E., Kohli, P., Hutto, P.W.: Causal memory: definitions, implementation, and programming. Distrib. Comput. 9(1), 37\u201349 (1995)","journal-title":"Distrib. Comput."},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7:1\u20137:74 (2014)","DOI":"10.1145\/2627752"},{"issue":"1\u20132","key":"8_CR6","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1999.2847","volume":"160","author":"R Alur","year":"2000","unstructured":"Alur, R., McMillan, K.L., Peled, D.A.: Model-checking of correctness conditions for concurrent objects. Inf. Comput. 160(1\u20132), 167\u2013188 (2000)","journal-title":"Inf. Comput."},{"key":"8_CR7","unstructured":"Anonymous. Ccchecker. Anonymized implementation"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Batty, M., Memarian, K., Owens, S., Sarkar, S., Sewell, P.: Clarifying and compiling C\/C++ concurrency: from C++11 to POWER. In: Field, J., Hicks, M. (eds.) Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, 22\u201328 January 2012, pp. 509\u2013520. ACM (2012)","DOI":"10.1145\/2103656.2103717"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, 26\u201328 January 2011, pp. 55\u201366. ACM (2011)","DOI":"10.1145\/1926385.1926394"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Enea, C., Guerraoui, R., Hamza, J.: On verifying causal consistency. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18\u201320 January 2017, pp. 626\u2013638. ACM (2017)","DOI":"10.1145\/3009837.3009888"},{"issue":"1\u20132","key":"8_CR11","first-page":"1","volume":"1","author":"S Burckhardt","year":"2014","unstructured":"Burckhardt, S.: Principles of eventual consistency. Found. Trends Program. Lang. 1(1\u20132), 1\u2013150 (2014)","journal-title":"Found. Trends Program. Lang."},{"issue":"3","key":"8_CR12","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1023\/A:1026276129010","volume":"23","author":"G Delzanno","year":"2003","unstructured":"Delzanno, G.: Constraint-based verification of parameterized cache coherence protocols. Formal Methods Syst. Des. 23(3), 257\u2013301 (2003)","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Dierl, S., Fiterau-Brostean, P., Howar, F., Jonsson, B., Sagonas, K., T\u00e5quist, F.: Scalable tree-based register automata learning. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024. LNCS, vol. 14571, pp. 87\u2013108. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57249-4_5","DOI":"10.1007\/978-3-031-57249-4_5"},{"issue":"1\u20132","key":"8_CR14","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! Theor. Comput. Sci. 256(1\u20132), 63\u201392 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Fiterau-Brostean, P., Jonsson, B., Sagonas, K., T\u00e5quist, F.: Automata-based automated detection of state machine bugs in protocol implementations. In: 30th Annual Network and Distributed System Security Symposium, NDSS 2023, San Diego, California, USA, 27 February\u20133 March 2023. The Internet Society (2023)","DOI":"10.14722\/ndss.2023.23068"},{"issue":"4","key":"8_CR16","doi-asserted-by":"publisher","first-page":"1208","DOI":"10.1137\/S0097539794279614","volume":"26","author":"PB Gibbons","year":"1997","unstructured":"Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comput. 26(4), 1208\u20131244 (1997)","journal-title":"SIAM J. Comput."},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C\/C++ concurrency. Proc. ACM Program. Lang. 2(POPL), 17:1\u201317:32 (2018)","DOI":"10.1145\/3158105"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Lahav, O., Vafeiadis, V.: Kater: automating weak memory model metatheory and consistency checking. Proc. ACM Program. Lang. 7(POPL), 544\u2013572 (2023)","DOI":"10.1145\/3571212"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Lahav, O., Boker, U.: What\u2019s decidable about causally consistent shared memory? ACM Trans. Program. Lang. Syst. 44(2), 8:1\u20138:55 (2022)","DOI":"10.1145\/3505273"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming release-acquire consistency. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20\u201322 January 2016, pp. 649\u2013662. ACM (2016)","DOI":"10.1145\/2837614.2837643"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Luo, W., Demsky, B.: C11tester: a race detector for C\/C++ atomics. In: Sherwood, T., Berger, E.D., Kozyrakis, C. (eds.) ASPLOS 2021: 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Virtual Event, USA, 19\u201323 April 2021, pp. 630\u2013646. ACM (2021)","DOI":"10.1145\/3445814.3446711"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Perrin, M., Most\u00e9faoui, A., Jard, C.: Causal consistency: beyond memory. In: Asenjo, R., Harris, T. (eds.) Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2016, Barcelona, Spain, 12\u201316 March 2016, pp. 26:1\u201326:12. ACM (2016)","DOI":"10.1145\/2851141.2851170"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"940","DOI":"10.1007\/978-3-319-89884-1_33","volume-title":"Programming Languages and Systems","author":"A Raad","year":"2018","unstructured":"Raad, A., Lahav, O., Vafeiadis, V.: On parallel snapshot isolation and release\/acquire consistency. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 940\u2013967. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_33"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Sarkar, S., et al.: Synchronising C\/C++ and POWER. In: Vitek, J., Lin, H., Tip, F. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2012, Beijing, China, 11\u201316 June 2012, pp. 311\u2013322. ACM (2012)","DOI":"10.1145\/2254064.2254102"},{"issue":"2","key":"8_CR25","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1145\/42190.42277","volume":"10","author":"D Shasha","year":"1988","unstructured":"Shasha, D., Snir, M.: Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst. 10(2), 282\u2013312 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Sovran, Y., Power, R., Aguilera, M.K., Li, J.: Transactional storage for geo-replicated systems. In: Wobber, T., Druschel, P. (eds.) Proceedings of the 23rd ACM Symposium on Operating Systems Principles 2011, SOSP 2011, Cascais, Portugal, 23\u201326 October 2011, pp. 385\u2013400. ACM (2011)","DOI":"10.1145\/2043556.2043592"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Tun\u00e7, H.C., Abdulla, P.A., Chakraborty, S., Krishna, S., Mathur, U., Pavlogiannis, A.: Optimal reads-from consistency checking for C11-style memory models. Proc. ACM Program. Lang. 7(PLDI), 761\u2013785 (2023)","DOI":"10.1145\/3591251"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2025"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-11176-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T11:09:24Z","timestamp":1770721764000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-11176-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,23]]},"ISBN":["9783032111753","9783032111760"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-11176-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,23]]},"assertion":[{"value":"23 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marrakesh","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Morocco","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2025.digital-hub.sh\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}