{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T01:15:39Z","timestamp":1769044539851,"version":"3.49.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2022,10,20]],"date-time":"2022-10-20T00:00:00Z","timestamp":1666224000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/R032351\/1"],"award-info":[{"award-number":["EP\/R032351\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/R032556\/1"],"award-info":[{"award-number":["EP\/R032556\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["No. EP\/V038915\/1"],"award-info":[{"award-number":["No. EP\/V038915\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/R025134\/2"],"award-info":[{"award-number":["EP\/R025134\/2"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"name":"ARC","award":["DP190102142"],"award-info":[{"award-number":["DP190102142"]}]},{"name":"DFG","award":["WE 2290\/14-1"],"award-info":[{"award-number":["WE 2290\/14-1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>\n            In this article, we propose an approach to program verification using an abstract characterisation of weak memory models. Our approach is based on a hierarchical axiom scheme that captures the\n            <jats:italic>observational properties<\/jats:italic>\n            of a memory model. In particular, we show that it is possible to prove correctness of a program with respect to a particular axiom scheme, and we show this proof to suffice for\n            <jats:italic>any<\/jats:italic>\n            memory model that satisfies the axioms. Our axiom scheme is developed using a characterisation of\n            <jats:italic>weakest liberal preconditions<\/jats:italic>\n            for weak memory. This characterisation naturally extends to Hoare logic and Owicki-Gries reasoning by lifting weakest liberal preconditions (defined over read\/write events) to the level of programs. We study three memory models (SC, TSO, and RC11-RAR) as example instantiations of the axioms, then we demonstrate the applicability of our reasoning technique on a number of litmus tests. The majority of the proofs in this article are supported by mechanisation within Isabelle\/HOL.\n          <\/jats:p>","DOI":"10.1145\/3545117","type":"journal-article","created":{"date-parts":[[2022,6,27]],"date-time":"2022-06-27T12:53:14Z","timestamp":1656334394000},"page":"1-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Unifying Operational Weak Memory Verification: An Axiomatic Approach"],"prefix":"10.1145","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8822-1091","authenticated-orcid":false,"given":"Simon","family":"Doherty","sequence":"first","affiliation":[{"name":"University of Sheffield, Sheffield, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8813-780X","authenticated-orcid":false,"given":"Sadegh","family":"Dalvandi","sequence":"additional","affiliation":[{"name":"University of Surrey, Guildford, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0446-3507","authenticated-orcid":false,"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[{"name":"University of Surrey, Guildford, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2385-7512","authenticated-orcid":false,"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[{"name":"University of Oldenburg, Oldenburg, Germany"}]}],"member":"320","published-online":{"date-parts":[[2022,10,20]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-016-0275-0"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314649"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_4"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_8"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276505"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009883"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_28"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.5555\/1642724"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_9"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429099"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_9"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_5"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454027"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_16"},{"key":"e_1_3_3_20_2","volume-title":"Proceedings of the ECOOP (LIPIcs)","author":"Dalvandi Sadegh","year":"2020","unstructured":"Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim. 2020. Owicki-gries reasoning for C11 RAR. In Proceedings of the ECOOP (LIPIcs), Robert Hirschfeld (Ed.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik."},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09610-2"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2016.02.003"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2011.159"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.6084\/m9.figshare.19779415"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3293883.3295702"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_20"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_17"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2874773"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_19"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2011.04.005"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428262"},{"key":"e_1_3_3_34_2","series-title":"Proceedings of the ECOOP","first-page":"17:1\u201317:29","volume":"74","author":"Kaiser Jan-Oliver","year":"2017","unstructured":"Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In Proceedings of the ECOOP(LIPIcs, Vol. 74), Peter M\u00fcller (Ed.). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 17:1\u201317:29."},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158105"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3326938.3326942"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_25"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78970"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386010"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/512976.512985"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.09.069"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2983997"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_22"},{"key":"e_1_3_3_51_2","unstructured":"Anton Podkopaev Ilya Sergey and Aleksandar Nanevski. 2016. Operational aspects of C\/C++ concurrency. Retrieved from arxiv:1606.01400."},{"key":"e_1_3_3_52_2","first-page":"1","volume-title":"Proceedings of the FMCAD","author":"Le\u00f3n Hern\u00e1n Ponce de","year":"2018","unstructured":"Hern\u00e1n Ponce de Le\u00f3n, Florian Furbach, Keijo Heljanko, and Roland Meyer. 2018. BMC with memory models as modules. In Proceedings of the FMCAD, Nikolaj Bj\u00f8rner and Arie Gurfinkel (Eds.). IEEE, 1\u20139."},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314624"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_11"},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_13"},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03077-7_21"},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009838"},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_13"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3545117","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3545117","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:44Z","timestamp":1750186964000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3545117"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,20]]},"references-count":60,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3545117"],"URL":"https:\/\/doi.org\/10.1145\/3545117","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,20]]},"assertion":[{"value":"2021-10-12","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-05-15","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-10-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}