{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T18:54:42Z","timestamp":1783018482009,"version":"3.54.6"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262035","type":"print"},{"value":"9783032262042","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,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"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                    Reasoning about concurrent programs executed on weak memory models is an inherently complex task. So far, existing proof calculi for weak memory models only cover\n                    <jats:italic>safety<\/jats:italic>\n                    properties. In this paper, we provide the first proof calculus for reasoning about\n                    <jats:italic>liveness<\/jats:italic>\n                    . Our proof calculus is based on Manna and Pnueli\u2019s proof rules for response under weak fairness, formulated in linear temporal logic. Our extension includes the incorporation of\n                    <jats:italic>memory fairness<\/jats:italic>\n                    into rules as well as the usage of\n                    <jats:italic>ranking functions<\/jats:italic>\n                    defined over weak memory state. We have applied our reasoning technique to the Ticket lock algorithm and have proved it to guarantee starvation freedom under memory models Release-Acquire and Strong Coherence for any number of concurrent threads.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_6","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:49:58Z","timestamp":1779032998000},"page":"109-129","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Proving Liveness on\u00a0Weak Memory"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-8778-9098","authenticated-orcid":false,"given":"Lara","family":"Bargmann","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2385-7512","authenticated-orcid":false,"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-031-56222-8_1","volume-title":"Taming the Infinities of Concurrency","author":"PA Abdulla","year":"2024","unstructured":"Abdulla, P.A., Atig, M.F., Godbole, A., Krishna, S.N., Vahanwala, M.: Fairness and liveness under weak consistency. In: Kiefer, S., K\u0159et\u00ednsk\u00fd, J., Ku\u010dera, A. (eds.) Taming the Infinities of Concurrency. LNCS, vol. 14660, pp. 1\u201321. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-56222-8_1"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-031-37706-8_10","volume-title":"Computer Aided Verification - CAV 2023","author":"PA Abdulla","year":"2023","unstructured":"Abdulla, P.A., Atig, M.F., Godbole, A., Krishna, S., Vahanwala, M.: Overcoming memory weakness with unified fairness. In: Enea, C., Lal, A. (eds.) CAV 2023. LNCS, vol. 13964, pp. 184\u2013205. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_10"},{"key":"6_CR3","doi-asserted-by":"publisher","unstructured":"Apt, K.R., de\u00a0Boer, F.S., Olderog, E.-R.: Proving Termination of Parallel Programs, pp. 1\u20136. Springer, New York (1990). https:\/\/doi.org\/10.1007\/978-1-4612-4476-9_1","DOI":"10.1007\/978-1-4612-4476-9_1"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-031-71162-6_27","volume-title":"Formal Methods - FM 2024","author":"L Bargmann","year":"2024","unstructured":"Bargmann, L., Dongol, B., Wehrheim, H.: Unifying weak memory verification using potentials. In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M. (eds.) FM 2024. LNCS, vol. 14933, pp. 519\u2013537. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_27"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Bargmann, L., Wehrheim, H.: Towards proving liveness on weak memory (extended version) (2026). https:\/\/doi.org\/10.48550\/arXiv.2602.19609","DOI":"10.48550\/arXiv.2602.19609"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-030-99336-8_9","volume-title":"Programming Languages and Systems - ESOP 2022","author":"EV Bila","year":"2022","unstructured":"Bila, E.V., Dongol, B., Lahav, O., Raad, A., Wickerson, J.: View-based Owicki-Gries reasoning for persistent x86-TSO. In: Sergey, I. (ed.) ESOP 2022. LNCS, vol. 13240, pp. 234\u2013261. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99336-8_9"},{"key":"6_CR7","doi-asserted-by":"publisher","unstructured":"Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269\u2013276 (1991). https:\/\/doi.org\/10.1016\/0020-0190(91)90122-X","DOI":"10.1016\/0020-0190(91)90122-X"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-031-66676-6_4","volume-title":"The Practice of Formal Methods","author":"RJ Colvin","year":"2024","unstructured":"Colvin, R.J., Hayes, I.J., Heiner, S., H\u00f6fner, P., Meinicke, L., Su, R.C.: Practical rely\/guarantee verification of an efficient lock for seL4 on multicore architectures. In: Cavalcanti, A., Baxter, J. (eds.) The Practice of Formal Methods. LNCS, vol. 14780, pp. 65\u201387. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-66676-6_4"},{"key":"6_CR9","doi-asserted-by":"publisher","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Proving thread termination. In: PLDI, pp. 320\u2013330. ACM (2007). https:\/\/doi.org\/10.1145\/1250734.1250771","DOI":"10.1145\/1250734.1250771"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Dalvandi, S., Doherty, S., Dongol, B., Wehrheim, H.: Owicki-Gries reasoning for C11 RAR. In: Hirschfeld, R., Pape, T. (eds.) ECOOP, LIPIcs, pp. 11:1\u201311:26. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2020.11","DOI":"10.4230\/LIPIcs.ECOOP.2020.11"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-030-45237-7_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Ponce-de-Le\u00f3n","year":"2020","unstructured":"Ponce-de-Le\u00f3n, H., Furbach, F., Heljanko, K., Meyer, R.: Dartagnan: bounded model checking for weak memory models (competition contribution). In: TACAS 2020. LNCS, vol. 12079, pp. 378\u2013382. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_24"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-030-72013-1_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Ponce-de-Le\u00f3n","year":"2021","unstructured":"Ponce-de-Le\u00f3n, H., Haas, T., Meyer, R.: Dartagnan: leveraging compiler optimizations and the price of precision (competition contribution). In: TACAS 2021. LNCS, vol. 12652, pp. 428\u2013432. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_26"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-031-66676-6_5","volume-title":"The Practice of Formal Methods","author":"B Dongol","year":"2024","unstructured":"Dongol, B., Lahav, O., Wehrheim, H.: A rely-guarantee framework for proving deadlock freedom under causal consistency. In: Cavalcanti, A., Baxter, J. (eds.) The Practice of Formal Methods. LNCS, vol. 14780, pp. 88\u2013108. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-66676-6_5"},{"key":"6_CR14","doi-asserted-by":"publisher","unstructured":"D\u2019Osualdo, E., Sutherland, J., Farzan, A., Gardner, P.: Tada live: compositional reasoning for termination of fine-grained concurrent programs. ACM Trans. Program. Lang. Syst. 43(4), 16:1\u201316:134 (2021). https:\/\/doi.org\/10.1145\/3477082","DOI":"10.1145\/3477082"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Haas, T., Meyer, R., de\u00a0Le\u00f3n, H.P., Gardu\u00f1o, A.L.: Recurrence sets for proving fair non-termination under axiomatic memory consistency models. Proc. ACM Program. Lang. 10(POPL), 1296\u20131325 (2026). https:\/\/doi.org\/10.1145\/3776687","DOI":"10.1145\/3776687"},{"key":"6_CR16","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":"6_CR17","doi-asserted-by":"crossref","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983). https:\/\/doi.org\/10.1145\/69575.69577","DOI":"10.1145\/69575.69577"},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"Kaiser, J.-O., Dang, H.-H., Dreyer, D., Lahav, O., Vafeiadis, V.: Strong logic for weak memory: reasoning about release-acquire consistency in iris. In: M\u00fcller, P. (ed.) ECOOP. LIPIcs, vol. 74, pp. 17:1\u201317:29. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2017.17","DOI":"10.4230\/LIPICS.ECOOP.2017.17"},{"key":"6_CR19","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/3505273","DOI":"10.1145\/3505273"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-031-37706-8_11","volume-title":"Computer Aided Verification - CAV 2023","author":"O Lahav","year":"2023","unstructured":"Lahav, O., Dongol, B., Wehrheim, H.: Rely-guarantee reasoning for causally consistent shared memory. In: Enea, C., Lal, A. (eds.) CAV 2023. LNCS, vol. 13964, pp. 206\u2013229. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_11"},{"key":"6_CR21","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":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-662-47666-6_25","volume-title":"Automata, Languages, and Programming","author":"O Lahav","year":"2015","unstructured":"Lahav, O., Vafeiadis, V.: Owicki-Gries reasoning for weak memory models. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 311\u2013323. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-47666-6_25"},{"key":"6_CR23","doi-asserted-by":"publisher","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690\u2013691 (1979). https:\/\/doi.org\/10.1109\/TC.1979.1675439","DOI":"10.1109\/TC.1979.1675439"},{"key":"6_CR24","doi-asserted-by":"publisher","unstructured":"Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci. 83(1), 91\u2013130 (1991). https:\/\/doi.org\/10.1016\/0304-3975(91)90041-Y","DOI":"10.1016\/0304-3975(91)90041-Y"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-13754-9_13","volume-title":"Time for Verification","author":"Z Manna","year":"2010","unstructured":"Manna, Z., Pnueli, A.: Temporal verification of reactive systems: response. In: Manna, Z., Peled, D.A. (eds.) Time for Verification. LNCS, vol. 6200, pp. 279\u2013361. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13754-9_13"},{"key":"6_CR26","doi-asserted-by":"publisher","unstructured":"Mellor-Crummey, J.M., Scott, M.L.: Algorithms for scalable synchronization on shared-memory multiprocessors. ACM Trans. Comput. Syst. 9(1), 21\u201365 (1991). https:\/\/doi.org\/10.1145\/103727.103729","DOI":"10.1145\/103727.103729"},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"Moszkowski, B.C.: A complete axiom system for propositional interval temporal logic with infinite time. Log. Methods Comput. Sci. 8(3) (2012). https:\/\/doi.org\/10.2168\/LMCS-8(3:10)2012","DOI":"10.2168\/LMCS-8(3:10)2012"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-642-03359-9_27","volume-title":"Theorem Proving in Higher Order Logics","author":"S Owens","year":"2009","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 391\u2013407. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_27"},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Inf. 6, 319\u2013340 (1976). https:\/\/doi.org\/10.1007\/BF00268134","DOI":"10.1007\/BF00268134"},{"key":"6_CR30","doi-asserted-by":"publisher","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. ACM Trans. Program. Lang. Syst. 29(3), 15 (2007). https:\/\/doi.org\/10.1145\/1232420.1232422","DOI":"10.1145\/1232420.1232422"},{"key":"6_CR31","doi-asserted-by":"publisher","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM 53(7), 89\u201397 (2010). https:\/\/doi.org\/10.1145\/1785414.1785443","DOI":"10.1145\/1785414.1785443"},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-031-21213-0_10","volume-title":"Dependable Software Engineering. Theories, Tools, and Applications - SETTA 2022","author":"C Wang","year":"2022","unstructured":"Wang, C., Petri, G., Lv, Y., Long, T., Liu, Z.: Decidability of liveness for concurrent objects on the TSO memory model. In: Dong, W., Talpin, J.P. (eds.) SETTA 2022. LNCS, vol. 13649, pp. 149\u2013165. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-21213-0_10"},{"key":"6_CR33","doi-asserted-by":"publisher","unstructured":"Qiwen, X., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Asp. Comput. 9(2), 149\u2013174 (1997). https:\/\/doi.org\/10.1007\/BF01211617","DOI":"10.1007\/BF01211617"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26204-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T17:47:04Z","timestamp":1783014424000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_6","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":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","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":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}