{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:39:46Z","timestamp":1742960386728,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030912642"},{"type":"electronic","value":"9783030912659"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-91265-9_5","type":"book-chapter","created":{"date-parts":[[2021,11,19]],"date-time":"2021-11-19T11:26:47Z","timestamp":1637321207000},"page":"81-101","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Trace Semantics and\u00a0Algebraic Laws for\u00a0MCA ARMv8 Architecture Based on\u00a0UTP"],"prefix":"10.1007","author":[{"given":"Lili","family":"Xiao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,11,18]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S., Sewell, P.: Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8. Proc. ACM Program. Lang. 2(POPL), 1\u201329 (2017)","key":"5_CR1","DOI":"10.1145\/3158107"},{"unstructured":"Pulte, C.: The Semantics of Multicopy Atomic ARMv8 and RISC-V. University of Cambridge (2019)","key":"5_CR2"},{"doi-asserted-by":"crossref","unstructured":"Flur, S., et al.: Modelling the ARMv8 architecture, operationally: concurrency and ISA. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 608\u2013621 (2016)","key":"5_CR3","DOI":"10.1145\/2837614.2837615"},{"key":"5_CR4","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":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-319-95582-7_14","volume-title":"Formal Methods","author":"RJ Colvin","year":"2018","unstructured":"Colvin, R.J., Smith, G.: A wide-spectrum language for verification of programs on weak memory models. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 240\u2013257. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_14"},{"key":"5_CR6","volume-title":"Unifying Theories of Programming","author":"CAR Hoare","year":"1998","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, Englewood Cliffs (1998)"},{"unstructured":"Plotkin, G.D.: A Structural Approach to Operational Semantics. Aarhus University (1981)","key":"5_CR7"},{"key":"5_CR8","volume-title":"Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory","author":"JE Stoy","year":"1981","unstructured":"Stoy, J.E.: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge (1981)"},{"issue":"8","key":"5_CR9","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/27651.27653","volume":"30","author":"CAR Hoare","year":"1987","unstructured":"Hoare, C.A.R., et al.: Laws of programming. Commun. ACM 30(8), 672\u2013686 (1987)","journal-title":"Commun. ACM"},{"key":"5_CR10","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.102308","volume":"184","author":"K Winter","year":"2019","unstructured":"Winter, K., Smith, G., Derrick, J.: Modelling concurrent objects running on the TSO and ARMv8 memory models. Sci. Comput. Program. 184, 102308 (2019)","journal-title":"Sci. Comput. Program."},{"key":"5_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s00165-019-00499-8","volume":"32","author":"G Smith","year":"2019","unstructured":"Smith, G., Winter, K., Colvin, R.J.: Linearizability on hardware weak memory models. Formal Aspects Comput. 32, 1\u201332 (2019)","journal-title":"Formal Aspects Comput."},{"doi-asserted-by":"crossref","unstructured":"Winter, K., Smith, G., Derrick, J.: Observational models for linearizability checking on weak memory models. In: International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 100\u2013107. IEEE (2018)","key":"5_CR12","DOI":"10.1109\/TASE.2018.00021"},{"key":"5_CR13","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/j.entcs.2018.03.025","volume":"336","author":"R Kavanagh","year":"2018","unstructured":"Kavanagh, R., Brookes, S.: A denotational semantics for SPARC TSO. Electron. Notes Theor. Comput. Sci. 336, 223\u2013239 (2018)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"unstructured":"Colvin, R.J., Smith, G.: A high-level operational semantics for hardware weak memory models, arXiv preprint arXiv:1812.00996 (2018)","key":"5_CR14"},{"issue":"2","key":"5_CR15","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1006\/inco.1996.0056","volume":"127","author":"S Brookes","year":"1996","unstructured":"Brookes, S.: Full abstraction for a shared-variable parallel language. Inf. Comput. 127(2), 145\u2013163 (1996)","journal-title":"Inf. Comput."},{"key":"5_CR16","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Hoboken (1985)"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/978-3-030-30942-8_32","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"G Smith","year":"2019","unstructured":"Smith, G., Coughlin, N., Murray, T.: Value-dependent information-flow security on weak memory models. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 539\u2013555. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_32"},{"issue":"3","key":"5_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2200\/S00346ED1V01Y201104CAC016","volume":"6","author":"DJ Sorin","year":"2011","unstructured":"Sorin, D.J., Hill, M.D., Wood, D.A.: A primer on memory consistency and cache coherence. Synthesis Lect. Comput. Archit. 6(3), 1\u2013212 (2011)","journal-title":"Synthesis Lect. Comput. Archit."},{"issue":"1","key":"5_CR19","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)","journal-title":"J. Logic Algebraic Program."},{"issue":"2","key":"5_CR20","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/0020-0190(93)90219-Y","volume":"45","author":"J He","year":"1993","unstructured":"He, J., Hoare, C.A.R.: From algebra to operational semantics. Inf. Process. Lett. 45(2), 75\u201380 (1993)","journal-title":"Inf. Process. Lett."},{"doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R., He, J., Sampaio, A.: Algebraic derivation of an operational semantics. In: Proof, Language, and Interaction: Essays in Honour of Robin Milner, pp. 77\u201398 (2000)","key":"5_CR21","DOI":"10.7551\/mitpress\/5641.003.0008"},{"issue":"3","key":"5_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3295699","volume":"28","author":"F Sheng","year":"2019","unstructured":"Sheng, F., Zhu, H., He, J., Yang, Z., Bowen, J.P.: Theoretical and practical aspects of linking operational and algebraic semantics for MDESL. ACM Trans. Softw. Eng. Methodol. (TOSEM) 28(3), 1\u201346 (2019)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"unstructured":"Huet, G., Kahn, G., Paulin-Mohring, C.: The Coq Proof Assistant a Tutorial (2005)","key":"5_CR23"},{"key":"5_CR24","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2013","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-91265-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T17:21:56Z","timestamp":1726161716000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-91265-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030912642","9783030912659"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-91265-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"18 November 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETTA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Beijing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 November 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 November 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setta2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/lcs.ios.ac.cn\/setta2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"39","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.05","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2.53","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}