{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T13:50:00Z","timestamp":1782913800361,"version":"3.54.5"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032273390","type":"print"},{"value":"9783032273406","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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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-27340-6_1","type":"book-chapter","created":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T13:28:54Z","timestamp":1782912534000},"page":"1-19","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Rely-Guarantee Verification of\u00a0Queue Locks with\u00a0Proof Support in\u00a0Isabelle\/HOL"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2149-675X","authenticated-orcid":false,"given":"Robert J.","family":"Colvin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3417-0350","authenticated-orcid":false,"given":"Scott","family":"Heiner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2141-5868","authenticated-orcid":false,"given":"Peter","family":"H\u00f6fner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0176-3264","authenticated-orcid":false,"given":"Roger C.","family":"Su","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,8,2]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Amani, S., Andronick, J., Bortin, M., Lewis, C., Rizkallah, C., Tuong, J.: Complx: a verification framework for concurrent imperative programs. In: Certified Programs and Proofs. pp. 138\u2013150 (2017). https:\/\/doi.org\/10.1145\/3018610.3018627","DOI":"10.1145\/3018610.3018627"},{"issue":"1","key":"1_CR2","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1109\/71.80120","volume":"1","author":"TE Anderson","year":"1990","unstructured":"Anderson, T.E.: The performance of spin lock alternatives for shared-memory multiprocessors. IEEE Trans. Parallel Distrib. Syst. 1(1), 6\u201315 (1990). https:\/\/doi.org\/10.1109\/71.80120","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-642-24364-6_2","volume-title":"Frontiers of Combining Systems","author":"JC Blanchette","year":"2011","unstructured":"Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle\/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 12\u201327. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24364-6_2"},{"issue":"4","key":"1_CR4","doi-asserted-by":"publisher","first-page":"807","DOI":"10.1093\/logcom\/exm030","volume":"17","author":"JW Coleman","year":"2007","unstructured":"Coleman, J.W., Jones, C.B.: A structural proof of the soundness of rely\/guarantee rules. J. Log. Comput. 17(4), 807\u2013841 (2007). https:\/\/doi.org\/10.1093\/logcom\/exm030","journal-title":"J. Log. Comput."},{"key":"1_CR5","doi-asserted-by":"publisher","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: The Practice of Formal Methods: Essays in Honour of Cliff Jones, Part I. pp. 65\u201387. LNCS 14780 (2024). https:\/\/doi.org\/10.1007\/978-3-031-66676-6_4","DOI":"10.1007\/978-3-031-66676-6_4"},{"issue":"5","key":"1_CR6","doi-asserted-by":"publisher","first-page":"853","DOI":"10.1007\/s00165-017-0416-4","volume":"29","author":"RJ Colvin","year":"2017","unstructured":"Colvin, R.J., Hayes, I.J., Meinicke, L.A.: Designing a semantic model for a wide-spectrum language with concurrency. Formal Aspects Comput. 29(5), 853\u2013875 (2017). https:\/\/doi.org\/10.1007\/s00165-017-0416-4","journal-title":"Formal Aspects Comput."},{"key":"1_CR7","unstructured":"Colvin, R.J., Heiner, S., H\u00f6fner, P., Su, R.C.: Rely-guarantee extensions and locks. Archive of Formal Proofs (2025). www.isa-afp.org\/entries\/RG_Locks.html, Formal proof development"},{"issue":"6","key":"1_CR8","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1109\/2.55501","volume":"23","author":"G Graunke","year":"1990","unstructured":"Graunke, G., Thakkar, S.: Synchronization algorithms for shared-memory multiprocessors. Computer 23(6), 60\u201369 (1990). https:\/\/doi.org\/10.1109\/2.55501","journal-title":"Computer"},{"issue":"6","key":"1_CR9","doi-asserted-by":"publisher","first-page":"1057","DOI":"10.1007\/s00165-016-0384-0","volume":"28","author":"IJ Hayes","year":"2016","unstructured":"Hayes, I.J.: Generalised rely-guarantee concurrency: an algebraic foundation. Formal Aspects Comput. 28(6), 1057\u20131078 (2016). https:\/\/doi.org\/10.1007\/s00165-016-0384-0","journal-title":"Formal Aspects Comput."},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Hayes, I.J., Meinicke, L.A., Evangelou-Oost, N.: Restructuring a concurrent refinement algebra. In: Relational and Algebraic Methods in Computer Science, pp. 135\u2013155 (2024). https:\/\/doi.org\/10.1007\/978-3-031-68279-7_9","DOI":"10.1007\/978-3-031-68279-7_9"},{"key":"1_CR11","unstructured":"Herlihy, M., Shavit, N., Luchangco, V., Spear, M.: The Art of Multiprocessor Programming, Morgan Kaufmann. 2 edn (2020)"},{"issue":"9","key":"1_CR12","doi-asserted-by":"publisher","first-page":"1622","DOI":"10.1016\/j.scico.2013.03.003","volume":"78","author":"WH Hesselink","year":"2013","unstructured":"Hesselink, W.H.: Mechanical verification of Lamport\u2019s bakery algorithm. Sci. Comput. Program. 78(9), 1622\u20131638 (2013). https:\/\/doi.org\/10.1016\/j.scico.2013.03.003","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"1_CR13","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","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","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-319-71237-6_14","volume-title":"Programming Languages and Systems","author":"J Kim","year":"2017","unstructured":"Kim, J., Sj\u00f6berg, V., Gu, R., Shao, Z.: Safety and liveness of MCS lock\u2014layer by layer. In: Chang, B.-Y.E. (ed.) APLAS 2017. LNCS, vol. 10695, pp. 273\u2013297. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-71237-6_14"},{"issue":"3","key":"1_CR15","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10817-015-9360-2","volume":"56","author":"D Matichuk","year":"2016","unstructured":"Matichuk, D., Murray, T., Wenzel, M.: Eisbach: a proof method language for Isabelle. J. Autom. Reason. 56(3), 261\u2013282 (2016). https:\/\/doi.org\/10.1007\/s10817-015-9360-2","journal-title":"J. Autom. Reason."},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-540-49020-3_13","volume-title":"Fundamental Approaches to Software Engineering","author":"T Nipkow","year":"1999","unstructured":"Nipkow, T., Nieto, L.P.: Owicki\/Gries in Isabelle\/HOL. In: Finance, J.-P. (ed.) FASE 1999. LNCS, vol. 1577, pp. 188\u2013203. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/978-3-540-49020-3_13"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-36575-3_24","volume-title":"Programming Languages and Systems","author":"LP Nieto","year":"2003","unstructured":"Nieto, L.P.: The rely-guarantee method in Isabelle\/HOL. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 348\u2013362. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36575-3_24"},{"key":"1_CR19","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.tcs.2022.03.030","volume":"919","author":"M Raynal","year":"2022","unstructured":"Raynal, M., Taubenfeld, G.: A visit to mutual exclusion in seven dates. Theor. Comput. Sci. 919, 47\u201365 (2022). https:\/\/doi.org\/10.1016\/j.tcs.2022.03.030","journal-title":"Theor. Comput. Sci."},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-030-81688-9_2","volume-title":"Computer Aided Verification","author":"T Reinhard","year":"2021","unstructured":"Reinhard, T., Jacobs, B.: Ghost signals: verifying termination of busy waiting. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 27\u201350. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_2"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/978-3-662-54577-5_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D San\u00e1n","year":"2017","unstructured":"San\u00e1n, D., Zhao, Y., Hou, Z., Zhang, F., Tiu, A., Liu, Y.: CSimpl: a rely-guarantee-based framework for verifying concurrent programs. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 481\u2013498. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_28"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Sanan, D., Zhao, Y., Lin, S.W., Yang, L.: CSim2: compositional top-down verification of concurrent systems using rely-guarantee. ACM Trans. Program. Lang. Syst. 43(1) (2021).https:\/\/doi.org\/10.1145\/3436808","DOI":"10.1145\/3436808"},{"key":"1_CR23","unstructured":"Schirmer, N.: A sequential imperative programming language syntax, semantics, Hoare logics and verification environment. Archive of Formal Proofs (2008). https:\/\/isa-afp.org\/entries\/Simpl.html, Formal proof development"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1007\/978-3-319-63387-9_27","volume-title":"Computer Aided Verification","author":"M Windsor","year":"2017","unstructured":"Windsor, M., Dodds, M., Simner, B., Parkinson, M.J.: Starling: lightweight concurrency verification with views. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 544\u2013569. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_27"},{"issue":"2","key":"1_CR25","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/s10817-018-9489-x","volume":"63","author":"Y Zakowski","year":"2018","unstructured":"Zakowski, Y., et al.: Verifying a concurrent garbage collector with a rely-guarantee methodology. J. Autom. Reason. 63(2), 489\u2013515 (2018). https:\/\/doi.org\/10.1007\/s10817-018-9489-x","journal-title":"J. Autom. Reason."}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-27340-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T13:29:01Z","timestamp":1782912541000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-27340-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032273390","9783032273406"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-27340-6_1","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":"2 August 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Menlo Park","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","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":"6 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/systemf.epfl.ch\/etc\/vstte2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}