{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:00:06Z","timestamp":1779087606105,"version":"3.51.4"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031666759","type":"print"},{"value":"9783031666766","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-66676-6_5","type":"book-chapter","created":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:04:18Z","timestamp":1725451458000},"page":"88-108","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Rely-Guarantee Framework for\u00a0Proving Deadlock Freedom Under Causal Consistency"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0446-3507","authenticated-orcid":false,"given":"Brijesh","family":"Dongol","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4305-6998","authenticated-orcid":false,"given":"Ori","family":"Lahav","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2385-7512","authenticated-orcid":false,"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,4]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Godbole, A., Krishna, S., Vahanwala, M.: Overcoming memory weakness with unified fairness - systematic verification of liveness in weak memory models. In: CAV, LNCS, vol. 13964, pp. 184\u2013205. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_10","DOI":"10.1007\/978-3-031-37706-8_10"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM TOPLAS 36(2), 7:1\u20137:74 (2014). https:\/\/doi.org\/10.1145\/2627752","DOI":"10.1145\/2627752"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Bila, E.V., Dongol, B., Lahav, O., Raad, A., Wickerson, J.: View-Based Owicki-Gries Reasoning for Persistent x86-TSO. In: ESOP. LNCS, vol. 13240, pp. 234\u2013261. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99336-8_9","DOI":"10.1007\/978-3-030-99336-8_9"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Coughlin, N., Winter, K., Smith, G.: Rely\/Guarantee reasoning for multicopy atomic weak memory models. In: FM. LNCS, vol. 13047, pp. 292\u2013310. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_16","DOI":"10.1007\/978-3-030-90870-6_16"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Coughlin, N., Winter, K., Smith, G.: Compositional reasoning for non-multicopy atomic architectures. For. Asp. Comp. (2022). https:\/\/doi.org\/10.1145\/3574137","DOI":"10.1145\/3574137"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Dalvandi, S., Doherty, S., Dongol, B., Wehrheim, H.: Owicki-Gries reasoning for C11 RAR. In: ECOOP. LIPIcs, vol.\u00a0166, pp. 11:1\u201311:26. Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2020.11","DOI":"10.4230\/LIPIcs.ECOOP.2020.11"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Dalvandi, S., Dongol, B., Doherty, S., Wehrheim, H.: Integrating Owicki-Gries for C11-style memory models into Isabelle\/HOL. J. Automated Reasoning 66(1), 141\u2013171 (2022). https:\/\/doi.org\/10.1007\/s10817-021-09610-2","DOI":"10.1007\/s10817-021-09610-2"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: POPL. pp. 287\u2013300. ACM (2013), https:\/\/doi.org\/10.1145\/2429069.2429104","DOI":"10.1145\/2480359.2429104"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Doherty, S., Dalvandi, S., Dongol, B., Wehrheim, H.: Unifying operational weak memory verification: An axiomatic approach. ACM TOCL 23(4), 27:1\u201327:39 (2022). https:\/\/doi.org\/10.1145\/3545117","DOI":"10.1145\/3545117"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Feijen, W.H.J., van Gasteren, A.J.M.: On a Method of Multiprogramming. Springer (1999). https:\/\/doi.org\/10.1007\/978-1-4757-3126-2","DOI":"10.1007\/978-1-4757-3126-2"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Feng, X.: Local rely-guarantee reasoning. In: POPL, pp. 315\u2013327. ACM (2009). https:\/\/doi.org\/10.1145\/1480881.1480922","DOI":"10.1145\/1480881.1480922"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Hayes, I.J., Jones, C.B., Meinicke, L.A.: Specifying and reasoning about shared-variable concurrency. In: Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday. LNCS, vol. 14080, pp. 110\u2013135. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-40436-8_5","DOI":"10.1007\/978-3-031-40436-8_5"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). https:\/\/doi.org\/10.1145\/363235.363259","DOI":"10.1145\/363235.363259"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM TOPLAS 5(4), 596\u2013619 (1983). https:\/\/doi.org\/10.1145\/69575.69577","DOI":"10.1145\/69575.69577"},{"key":"5_CR15","unstructured":"Kaiser, J., Dang, H., Dreyer, D., Lahav, O., Vafeiadis, V.: Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In: ECOOP. LIPIcs, vol.\u00a074, pp. 17:1\u201317:29. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Lahav, O., Boker, U.: Decidable verification under a causally consistent shared memory. In: PLDI, pp. 211\u2013226. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385966","DOI":"10.1145\/3385412.3385966"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Lahav, O., Boker, U.: What\u2019s decidable about causally consistent shared memory? ACM TOPLAS 44(2), 8:1\u20138:55 (2022). https:\/\/doi.org\/10.1145\/3505273","DOI":"10.1145\/3505273"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Lahav, O., Dongol, B., Wehrheim, H.: Rely-guarantee reasoning for causally consistent shared memory. In: CAV. LNCS, vol. 13964, pp. 206\u2013229. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_11","DOI":"10.1007\/978-3-031-37706-8_11"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Lahav, O., Namakonov, E., Oberhauser, J., Podkopaev, A., Vafeiadis, V.: Making weak memory models fair. Proc. ACM Program. Lang. 5(OOPSLA), 1\u201327 (2021). https:\/\/doi.org\/10.1145\/3485475","DOI":"10.1145\/3485475"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Lahav, O., Vafeiadis, V.: Owicki-Gries reasoning for weak memory models. In: ICALP. LNCS, vol.\u00a09135, pp. 311\u2013323. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-47666-6_25","DOI":"10.1007\/978-3-662-47666-6_25"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Liang, H., Feng, X.: A program logic for concurrent objects under fair scheduling. SIGPLAN Not. 51(1), 385-399 (jan 2016). https:\/\/doi.org\/10.1145\/2914770.2837635","DOI":"10.1145\/2914770.2837635"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Meinicke, L.A., Hayes, I.J.: Using cylindric algebra to support local variables in rely\/guarantee concurrency. In: FormaliSE, pp. 108\u2013119. IEEE (2023). https:\/\/doi.org\/10.1109\/FORMALISE58978.2023.00019","DOI":"10.1109\/FORMALISE58978.2023.00019"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Oberhauser, J., Chehab, R.L.d.L., Behrens, D., Fu, M., Paolillo, A., Oberhauser, L., Bhat, K., Wen, Y., Chen, H., Kim, J., Vafeiadis, V.: Vsync: push-button verification and optimization for synchronization primitives on weak memory models. In: ASPLOS, pp. 530-545. ACM, New York (2021), https:\/\/doi.org\/10.1145\/3445814.3446748","DOI":"10.1145\/3445814.3446748"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6, 319\u2013340 (1976). https:\/\/doi.org\/10.1007\/BF00268134","DOI":"10.1007\/BF00268134"},{"key":"5_CR25","unstructured":"Qiwen, X.: A theory of state-based parallel programming. Ph.D. thesis, University of Oxford, UK (1992)"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Ridge, T.: A rely-guarantee proof system for x86-TSO. In: VSTTE. LNCS, vol.\u00a06217, pp. 55\u201370 (2010). https:\/\/doi.org\/10.1007\/978-3-642-15057-9_4","DOI":"10.1007\/978-3-642-15057-9_4"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Schellhorn, G., Tofan, B., Ernst, G., Pf\u00e4hler, J., Reif, W.: RGITL: A temporal logic framework for compositional reasoning about interleaved programs. Ann. Math. Artif. Intell. 71(1-3), 131\u2013174 (2014). https:\/\/doi.org\/10.1007\/s10472-013-9389-z","DOI":"10.1007\/s10472-013-9389-z"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Travkin, O., Wehrheim, H.: Towards a thread-local proof technique for starvation freedom. In: iFM. LNCS, vol.\u00a09681, pp. 193\u2013209. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_13","DOI":"10.1007\/978-3-319-33693-0_13"},{"key":"5_CR29","doi-asserted-by":"publisher","unstructured":"Singh, A.K., Lahav, O.: Decidable verification under localized release-acquire concurrency. In: TACAS. LNCS, vol. 14572, pp. 235\u2013254. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_12","DOI":"10.1007\/978-3-031-57256-2_12"},{"key":"5_CR30","unstructured":"St\u00f8len, K.: Development of Parallel Programs on Shared Data-structures. Ph.D. thesis, Computer Science Department, Manchester University (1990)"},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"Vafeiadis, V., Parkinson, M.J.: A marriage of rely\/guarantee and separation logic. In: CONCUR. LNCS, vol.\u00a04703, pp. 256\u2013271. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_18","DOI":"10.1007\/978-3-540-74407-8_18"},{"key":"5_CR32","doi-asserted-by":"publisher","unstructured":"Wright, D., Batty, M., Dongol, B.: Owicki-gries reasoning for C11 programs with relaxed dependencies. In: FM. LNCS, vol. 13047, pp. 237\u2013254. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_13","DOI":"10.1007\/978-3-030-90870-6_13"},{"key":"5_CR33","doi-asserted-by":"publisher","unstructured":"Xu, Q., de\u00a0Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. For. Asp. Comp. 9(2), 149\u2013174 (1997). https:\/\/doi.org\/10.1007\/BF01211617","DOI":"10.1007\/BF01211617"}],"container-title":["Lecture Notes in Computer Science","The Practice of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66676-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:05:12Z","timestamp":1725451512000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66676-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031666759","9783031666766"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66676-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"4 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}