{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T16:29:30Z","timestamp":1783960170407,"version":"3.55.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031666728","type":"print"},{"value":"9783031666735","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-66673-5_11","type":"book-chapter","created":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:04:18Z","timestamp":1725451458000},"page":"206-225","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Modelling and\u00a0Verifying Programs Under the\u00a0Total Store Order Memory Model in\u00a0an\u00a0Algebraic Semantics Style"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9006-6219","authenticated-orcid":false,"given":"Lili","family":"Xiao","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0214-8565","authenticated-orcid":false,"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8748-6140","authenticated-orcid":false,"given":"Jonathan P.","family":"Bowen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3923-7972","authenticated-orcid":false,"given":"Sini","family":"Chen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,9,4]]},"reference":[{"key":"11_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 Informatica 54, 789\u2013818 (2017). https:\/\/doi.org\/10.1007\/s00236-016-0275-0","journal-title":"Acta Informatica"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-44881-0_7","volume-title":"Rewriting Techniques and Applications","author":"M Clavel","year":"2003","unstructured":"Clavel, M., et al.: The Maude 2.0 system. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 76\u201387. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44881-0_7"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Hayes, I.J., Jones, C.B., Meinicke, L.A.: Specifying and reasoning about shared-variable concurrency. In: Bowen, J.P., Li, Q., Xu, Q. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 14080, pp. 110\u2013135. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-40436-8_5","DOI":"10.1007\/978-3-031-40436-8_5"},{"key":"11_CR4","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998). http:\/\/www.unifyingtheories.org"},{"key":"11_CR5","unstructured":"Jones, C.B.: Development Methods for Computer Programs Including a Notion of Interference. Technical Monograph PRG-25, Programming Research Group, Oxford University Computing Laboratory (1981). https:\/\/www.cs.ox.ac.uk\/files\/9025\/PRG-25.pdf"},{"key":"11_CR6","unstructured":"Jones, C.B.: Systematic Software Development using VDM, 2nd edn. Prentice Hall International Series in Computer Science (1990)"},{"key":"11_CR7","doi-asserted-by":"publisher","first-page":"1121","DOI":"10.1007\/s00165-017-0446-y","volume":"29","author":"CB Jones","year":"2017","unstructured":"Jones, C.B.: The Turing Guide [book review]. Formal Aspects Comput. 29, 1121\u20131122 (2017). https:\/\/doi.org\/10.1007\/s00165-017-0446-y","journal-title":"Formal Aspects Comput."},{"key":"11_CR8","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-030-59257-8_7","volume-title":"Understanding Programming Languages","author":"CB Jones","year":"2020","unstructured":"Jones, C.B.: Other semantic approaches. In: Understanding Programming Languages, pp. 95\u2013117. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59257-8_7"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Jones, C.B., Misra, J.: Finding effective abstractions. In: Jones, C.B., Misra, J. (eds.) Theories of Programming: The Life and Works of Tony Hoare, chap. 2, pp. 23\u201340. Association for Computing Machinery (2021). https:\/\/doi.org\/10.1145\/3477355","DOI":"10.1145\/3477355"},{"issue":"1","key":"11_CR10","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1145\/3009837.3009850","volume":"52","author":"J Kang","year":"2017","unstructured":"Kang, J., Hur, C.K., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. ACM SIGPLAN Not. 52(1), 175\u2013189 (2017). https:\/\/doi.org\/10.1145\/3009837.3009850","journal-title":"ACM SIGPLAN Not."},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Kavanagh, R., Brookes, S.: A denotational semantics for SPARC TSO. Log. Meth. Comput. Sci. 15(2) (2019). https:\/\/doi.org\/10.23638\/LMCS-15(2:10)2019","DOI":"10.23638\/LMCS-15(2:10)2019"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-48989-6_29","volume-title":"FM 2016: Formal Methods","author":"O Lahav","year":"2016","unstructured":"Lahav, O., Vafeiadis, V.: Explaining relaxed memory models with program transformations. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 479\u2013495. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_29"},{"key":"11_CR13","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1016\/S1571-0661(04)00040-4","volume":"4","author":"N Mart\u00ed-Oliet","year":"1996","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. Electron. Notes Theor. Comput. Sci. 4, 190\u2013225 (1996). https:\/\/doi.org\/10.1016\/S1571-0661(04)00040-4","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"2","key":"11_CR14","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/S0304-3975(01)00357-7","volume":"285","author":"N Mart\u00ed-Oliet","year":"2002","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: Rewriting logic: roadmap and bibliography. Theoret. Comput. Sci. 285(2), 121\u2013154 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(01)00357-7","journal-title":"Theoret. Comput. Sci."},{"issue":"7\u20138","key":"11_CR15","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Logic Algebraic Program. 81(7\u20138), 721\u2013781 (2012). https:\/\/doi.org\/10.1016\/j.jlap.2012.06.003","journal-title":"J. Logic Algebraic Program."},{"issue":"2","key":"11_CR16","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1109\/MAHC.1984.10017","volume":"6","author":"FL Morris","year":"1984","unstructured":"Morris, F.L., Jones, C.B.: An early proof by Alan Turing. IEEE Ann. Hist. Comput. 6(2), 139\u2013143 (1984). https:\/\/doi.org\/10.1109\/MAHC.1984.10017","journal-title":"IEEE Ann. Hist. Comput."},{"key":"11_CR17","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"},{"issue":"4","key":"11_CR18","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1109\/MC.1996.488298","volume":"29","author":"H Saiedian","year":"1996","unstructured":"Saiedian, H., et al.: An invitation to formal methods. Computer 29(4), 16\u201330 (1996). https:\/\/doi.org\/10.1109\/MC.1996.488298","journal-title":"Computer"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Sorin, D., Hill, M., Wood, D.: A Primer on Memory Consistency and Cache Coherence. Morgan & Claypool Publishers, San Rafael (2011)","DOI":"10.1007\/978-3-031-01733-9"},{"issue":"6","key":"11_CR20","doi-asserted-by":"publisher","first-page":"1269","DOI":"10.1007\/s11390-021-1616-1","volume":"36","author":"L Xiao","year":"2021","unstructured":"Xiao, L., Zhu, H., Xu, Q.: Trace semantics and algebraic laws for total store order memory model. J. Comput. Sci. Technol. 36(6), 1269\u20131290 (2021). https:\/\/doi.org\/10.1007\/s11390-021-1616-1","journal-title":"J. Comput. Sci. Technol."},{"key":"11_CR21","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/s11334-009-0100-9","volume":"5","author":"H Zhu","year":"2009","unstructured":"Zhu, H., Qin, S., He, J., Bowen, J.P.: PTSC: probability, time and shared-variable concurrency. Innovations Syst. Softw. Eng. 5, 271\u2013284 (2009). https:\/\/doi.org\/10.1007\/s11334-009-0100-9","journal-title":"Innovations Syst. Softw. Eng."},{"issue":"1","key":"11_CR22","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.jlap.2011.06.003","volume":"81","author":"H Zhu","year":"2012","unstructured":"Zhu, H., Yang, F., He, J., Bowen, J.P., Sanders, J.W., Qin, S.: Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language. J. Logic Algebraic Program. 81(1), 2\u201325 (2012). https:\/\/doi.org\/10.1016\/j.jlap.2011.06.003","journal-title":"J. Logic Algebraic Program."}],"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-66673-5_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:08:41Z","timestamp":1725451721000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66673-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031666728","9783031666735"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66673-5_11","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"}}]}}