{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T01:02:47Z","timestamp":1768870967923,"version":"3.49.0"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,11,16]],"date-time":"2021-11-16T00:00:00Z","timestamp":1637020800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,11,16]],"date-time":"2021-11-16T00:00:00Z","timestamp":1637020800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["WE 2290\/12-1"],"award-info":[{"award-number":["WE 2290\/12-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R032556\/1"],"award-info":[{"award-number":["EP\/R032556\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R032351\/1"],"award-info":[{"award-number":["EP\/R032351\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Weak memory presents a new challenge for program verification and has resulted in the development of a variety of specialised logics. For C11-style memory models, our previous work has shown that it is possible to extend Hoare logic and Owicki\u2013Gries reasoning to verify correctness of weak memory programs. The technique introduces a set of high-level assertions over C11 states together with a set of basic Hoare-style axioms over atomic weak memory statements (e.g. reads\/writes), but retains all other standard proof obligations for compound statements. This paper takes this line of work further by introducing the first deductive verification environment in Isabelle\/HOL for C11-like weak memory programs. This verification environment is built on the Nipkow and Nieto\u2019s encoding of Owicki\u2013Gries in the Isabelle theorem prover. We exemplify our techniques over several litmus tests from the literature and two non-trivial examples: Peterson\u2019s algorithm and a read\u2013copy\u2013update algorithm adapted for C11. For the examples we consider, the proof outlines can be automatically discharged using the existing Isabelle tactics developed by Nipkow and Nieto. The benefit here is that programs can be written using a familiar pseudocode syntax with assertions embedded directly into the program.\n<\/jats:p>","DOI":"10.1007\/s10817-021-09610-2","type":"journal-article","created":{"date-parts":[[2021,11,16]],"date-time":"2021-11-16T06:04:17Z","timestamp":1637042657000},"page":"141-171","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Integrating Owicki\u2013Gries for C11-Style Memory Models into Isabelle\/HOL"],"prefix":"10.1007","volume":"66","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8813-780X","authenticated-orcid":false,"given":"Sadegh","family":"Dalvandi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0446-3507","authenticated-orcid":false,"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[]},{"given":"Simon","family":"Doherty","sequence":"additional","affiliation":[]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,11,16]]},"reference":[{"issue":"8","key":"9610_CR1","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1007\/s00236-016-0275-0","volume":"54","author":"PA Abdulla","year":"2017","unstructured":"Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. Acta Inf. 54(8), 789\u2013818 (2017)","journal-title":"Acta Inf."},{"key":"9610_CR2","doi-asserted-by":"crossref","unstructured":"Alglave, J., Cousot, P.: Ogre and Pythia: an invariance proof method for weak consistency models. In: Castagna, G., Gordon, A.D. (eds.) POPL, pp. 3\u201318. ACM (2017)","DOI":"10.1145\/3093333.3009883"},{"key":"9610_CR3","doi-asserted-by":"crossref","unstructured":"Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: Felleisen, M. Gardner, P. (eds.) ESOP, LNCS, vol. 7792, pp. 512\u2013532. Springer (2013)","DOI":"10.1007\/978-3-642-37036-6_28"},{"key":"9610_CR4","doi-asserted-by":"crossref","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Sharygina, N., Veith, H. (eds.) CAV, LNCS, vol. 8044, pp. 141\u2013157. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"9610_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5","volume-title":"Verification of Sequential and Concurrent Programs. Texts in Computer Science","author":"KR Apt","year":"2009","unstructured":"Apt, K.R., de Boer, F.S., Olderog, E.: Verification of Sequential and Concurrent Programs. Texts in Computer Science. Springer, Berlin (2009)"},{"key":"9610_CR6","doi-asserted-by":"crossref","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 55\u201366. ACM (2011)","DOI":"10.1145\/1925844.1926394"},{"key":"9610_CR7","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: judgement day. In: IJCAR, Lecture Notes in Computer Science, vol. 6173, pp. 107\u2013121. Springer (2010)","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"9610_CR8","doi-asserted-by":"crossref","unstructured":"Dalvandi, M., Dongol, B.: Towards deductive verification of C11 programs with Event-B and ProB. In: Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, p.\u00a04. ACM (2019)","DOI":"10.1145\/3340672.3341117"},{"key":"9610_CR9","doi-asserted-by":"publisher","unstructured":"Dalvandi, S., Doherty, S., Dongol, B., Wehrheim, H.: Owicki\u2013Gries reasoning for C11 RAR. In: Hirschfeld, R., Pape, T. (eds.) ECOOP, LIPIcs, vol. 166, 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":"9610_CR10","doi-asserted-by":"publisher","unstructured":"Dalvandi, S., Doherty, S., Dongol, B., Wehrheim, H.: Isabelle files for \"Integrating Owicki\u2013Gries for C11-style memory models into Isabelle\/HOL\" (2021). https:\/\/doi.org\/10.6084\/m9.figshare.14387201.v1. https:\/\/figshare.com\/articles\/software\/Isabelle_Files_for_Integrating_Owicki-Gries_for_C11-Style_Memory_Models_into_Isabelle_HOL_\/14387201","DOI":"10.6084\/m9.figshare.14387201.v1"},{"key":"9610_CR11","first-page":"62","volume":"47","author":"A Dan","year":"2017","unstructured":"Dan, A., Meshman, Y., Vechev, M., Yahav, E.: Effective abstractions for verification under relaxed memory models. Comput. Lang. Syst. Struct. 47, 62\u201376 (2017)","journal-title":"Comput. Lang. Syst. Struct."},{"key":"9610_CR12","volume-title":"Concurrency Verification: Introduction to Compositional and Noncompositional Methods, Cambridge Tracts in Theoretical Computer Science","author":"WP de Roever","year":"2001","unstructured":"de Roever, W.P., de Boer, F.S., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods, Cambridge Tracts in Theoretical Computer Science, vol. 54. Cambridge University Press, Cambridge (2001)"},{"issue":"2","key":"9610_CR13","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1109\/TPDS.2011.159","volume":"23","author":"M Desnoyers","year":"2012","unstructured":"Desnoyers, M., McKenney, P.E., Stern, A.S., Dagenais, M.R., Walpole, J.: User-level implementations of read-copy update. IEEE Trans. Parallel Distrib. Syst. 23(2), 375\u2013382 (2012). https:\/\/doi.org\/10.1109\/TPDS.2011.159","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"9610_CR14","doi-asserted-by":"crossref","unstructured":"Doherty, S., Dongol, B., Wehrheim, H., Derrick, J.: Verifying C11 programs operationally. In: Hollingsworth, J.K., Keidar, I. (eds.) PPoPP, pp. 355\u2013365. ACM (2019)","DOI":"10.1145\/3293883.3295702"},{"key":"9610_CR15","doi-asserted-by":"crossref","unstructured":"Doko, M., Vafeiadis, V.: A program logic for C11 memory fences. In: VMCAI, LNCS, vol. 9583, pp. 413\u2013430. Springer (2016)","DOI":"10.1007\/978-3-662-49122-5_20"},{"key":"9610_CR16","doi-asserted-by":"crossref","unstructured":"Doko, M., Vafeiadis, V.: Tackling real-life relaxed concurrency with FSL++. In: ESOP, pp. 448\u2013475 (2017)","DOI":"10.1007\/978-3-662-54434-1_17"},{"key":"9610_CR17","doi-asserted-by":"crossref","unstructured":"Dolan, S., Sivaramakrishnan, K., Madhavapeddy, A.: Bounding data races in space and time. In: PLDI, PLDI 2018, pp. 242\u2013255. ACM, New York, NY, USA (2018)","DOI":"10.1145\/3296979.3192421"},{"key":"9610_CR18","doi-asserted-by":"publisher","unstructured":"Gavrilenko, N., Ponce de Le\u2019on, H., Furbach, F., Heljanko, K., Meyer, R.: BMC for weak memory models: relation analysis for compact SMT encodings. In: Dillig, I., Tasiran, S. (eds.) CAV, LNCS, vol. 11561, pp. 355\u2013365. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_19","DOI":"10.1007\/978-3-030-25540-4_19"},{"issue":"10","key":"9610_CR19","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"issue":"2","key":"9610_CR20","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/s10270-012-0230-7","volume":"12","author":"B Jeannet","year":"2013","unstructured":"Jeannet, B.: Relational interprocedural verification of concurrent programs. Softw. Syst. Model. 12(2), 285\u2013306 (2013)","journal-title":"Softw. Syst. Model."},{"key":"9610_CR21","unstructured":"Kaiser, J., Dang, 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.\u00a074, pp. 17:1\u201317:29. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)"},{"key":"9610_CR22","doi-asserted-by":"crossref","unstructured":"Kang, J., Hur, C., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. In: POPL, pp. 175\u2013189. ACM (2017)","DOI":"10.1145\/3093333.3009850"},{"key":"9610_CR23","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C\/C++ concurrency. PACMPL 2(POPL), 17:1\u201317:32 (2018)","DOI":"10.1145\/3158105"},{"key":"9610_CR24","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Raad, A., Vafeiadis, V.: Model checking for weakly consistent libraries. In: McKinley, K.S., Fisher, K. (eds.) PLDI, pp. 96\u2013110. ACM (2019)","DOI":"10.1145\/3314221.3314609"},{"issue":"2","key":"9610_CR25","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1145\/3326938.3326942","volume":"6","author":"O Lahav","year":"2019","unstructured":"Lahav, O.: Verification under causally consistent shared memory. SIGLOG News 6(2), 43\u201356 (2019)","journal-title":"SIGLOG News"},{"key":"9610_CR26","doi-asserted-by":"crossref","unstructured":"Lahav, O., Vafeiadis, V.: Owicki\u2013Gries reasoning for weak memory models. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP, LNCS, vol. 9135, pp. 311\u2013323. Springer (2015)","DOI":"10.1007\/978-3-662-47666-6_25"},{"key":"9610_CR27","doi-asserted-by":"crossref","unstructured":"Lahav, O., Vafeiadis, V., Kang, J., Hur, C., Dreyer, D.: Repairing sequential consistency in C\/C++11. In: PLDI, pp. 618\u2013632. ACM (2017)","DOI":"10.1145\/3140587.3062352"},{"issue":"9","key":"9610_CR28","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"9610_CR29","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 41\u201362. Springer (2016)","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"9610_CR30","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Nieto, L.P.: Owicki\/Gries in Isabelle\/HOL. In: FASE, Lecture Notes in Computer Science, vol. 1577, pp. 188\u2013203. Springer (1999)","DOI":"10.1007\/978-3-540-49020-3_13"},{"key":"9610_CR31","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"SS Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Inf. 6, 319\u2013340 (1976)","journal-title":"Acta Inf."},{"key":"9610_CR32","unstructured":"Paulson, L.C.: Isabelle\u2014A Generic Theorem Prover (with a contribution by T. Nipkow), LNCS, vol. 828. Springer (1994)"},{"key":"9610_CR33","doi-asserted-by":"publisher","unstructured":"Paviotti, M., Cooksey, S., Paradis, A., Wright, D., Owens, S., Batty, M.: Modular relaxed dependencies in weak memory concurrency. In: M\u00fcller, P. (ed.) ESOP, LNCS, vol. 12075, pp. 599\u2013625. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-44914-8_22","DOI":"10.1007\/978-3-030-44914-8_22"},{"key":"9610_CR34","unstructured":"Podkopaev, A., Sergey, I., Nanevski, A.: Operational aspects of C\/C++ concurrency. CoRR abs\/1606.01400 (2016) . https:\/\/arxiv.org\/abs\/1606.01400"},{"key":"9610_CR35","doi-asserted-by":"crossref","unstructured":"Ponce de Le\u00f3n, H., Furbach, F., Heljanko, K., Meyer, R.: BMC with memory models as modules. In: Bj\u00f8rner, N., Gurfinkel, A. (eds.) FMCAD, pp. 1\u20139. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603021"},{"key":"9610_CR36","doi-asserted-by":"crossref","unstructured":"Summers, A.J., M\u00fcller, P.: Automating deductive verification for weak-memory programs. In: Beyer, D., Huisman, M. (eds.) TACAS, LNCS, vol. 10805, pp. 190\u2013209. Springer (2018)","DOI":"10.1007\/978-3-319-89960-2_11"},{"key":"9610_CR37","doi-asserted-by":"crossref","unstructured":"Svendsen, K., Pichon-Pharabod, J., Doko, M., Lahav, O., Vafeiadis, V.: A separation logic for a promising semantics. In: Ahmed, A. (ed.) ESOP, LNCS, vol. 10801, pp. 357\u2013384. Springer (2018)","DOI":"10.1007\/978-3-319-89884-1_13"},{"key":"9610_CR38","doi-asserted-by":"crossref","unstructured":"Travkin, O., M\u00fctze, A., Wehrheim, H.: SPIN as a linearizability checker under weak memory models. In: Bertacco, V. Legay, A. (eds.) HVC, LNCS, vol. 8244, pp. 311\u2013326. Springer (2013)","DOI":"10.1007\/978-3-319-03077-7_21"},{"key":"9610_CR39","doi-asserted-by":"crossref","unstructured":"Turon, A., Vafeiadis, V., Dreyer, D.: GPS: navigating weak memory with ghosts, protocols, and separation. In: Black, A.P., Millstein, T.D. (eds.) OOPSLA, pp. 691\u2013707. ACM (2014)","DOI":"10.1145\/2714064.2660243"},{"key":"9610_CR40","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, pp. 867\u2013884 (2013)","DOI":"10.1145\/2509136.2509532"},{"key":"9610_CR41","unstructured":"Williams, A.: https:\/\/www.justsoftwaresolutions.co.uk\/threading\/petersons_lock_with_C++0x_atomics.html (2018). Accessed 20 June 2018"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09610-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-021-09610-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09610-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,11]],"date-time":"2022-01-11T07:05:45Z","timestamp":1641884745000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-021-09610-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,16]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,2]]}},"alternative-id":["9610"],"URL":"https:\/\/doi.org\/10.1007\/s10817-021-09610-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,11,16]]},"assertion":[{"value":"11 September 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 September 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 November 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}