{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T17:57:31Z","timestamp":1743011851323,"version":"3.40.3"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319216676"},{"type":"electronic","value":"9783319216683"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21668-3_24","type":"book-chapter","created":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T11:08:53Z","timestamp":1436785733000},"page":"413-428","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["An Axiomatic Specification for Sequential Memory Models"],"prefix":"10.1007","author":[{"given":"William","family":"Mansky","sequence":"first","affiliation":[]},{"given":"Dmitri","family":"Garbuzov","sequence":"additional","affiliation":[]},{"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"24_CR1","unstructured":"Higham, L., Kawash, J., Verwaal, N.: Defining and comparing memory consistency models. In: Proceedings of the 10th International Conference on Parallel and Distributed Computing Systems, pp. 349\u2013356 (1997)"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"Kang, J., Hur, C., Mansky, W., Garbuzov, D., Zdancewic, S., Vafeiadis, V.: A formal C memory model supporting integer-pointer casts. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015 (to appear)","DOI":"10.1145\/2737924.2738005"},{"key":"24_CR3","unstructured":"Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis & transformation. In: Proceedings of the international symposium on Code generation and optimization: feedback-directed and runtime optimization, CGO 2004, p. 75. IEEE Computer Society, Washington, DC (2004). \n                      http:\/\/dl.acm.org\/citation.cfm?id=977395.977673"},{"issue":"4","key":"24_CR4","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reason 43(4), 363\u2013446 (2009). \n                      http:\/\/dx.doi.org\/10.1007\/s10817-009-9155-4","journal-title":"J. Autom. Reason"},{"key":"24_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X Leroy","year":"2008","unstructured":"Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. J. Autom. Reason 41, 1\u201331 (2008). \n                      http:\/\/dl.acm.org\/citation.cfm?id=1388522.1388533","journal-title":"J. Autom. Reason"},{"key":"24_CR6","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)"},{"key":"24_CR7","unstructured":"Saraswat, V.A., Jagadeesan, R., Michael, M., von Praun, C.: A theory of memory models. In: Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2007, pp. 161\u2013172. ACM, New York, NY (2007). \n                      http:\/\/doi.acm.org\/10.1145\/1229428.1229469"},{"key":"24_CR8","unstructured":"Stewart, G., Beringer, L., Cuellar, S., Appel, A.W.: Compositional compcert. In: Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, pp. 275\u2013287. ACM, New York, NY (2015). \n                      http:\/\/doi.acm.org\/10.1145\/2676726.2676985"},{"issue":"3","key":"24_CR9","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1145\/2487241.2487248","volume":"60","author":"J \u0160ev\u010d\u00edk","year":"2013","unstructured":"\u0160ev\u010d\u00edk, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S., Sewell, P.: CompCertTSO: a verified compiler for relaxed-memory concurrency. J. ACM 60(3), 221\u20132250 (2013). \n                      http:\/\/doi.acm.org\/10.1145\/2487241.2487248","journal-title":"J. ACM"},{"key":"24_CR10","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Nemos: a framework for axiomatic and executable specifications of memory consistency models. In: Proceedings of 18th International Parallel and Distributed Processing Symposium, p. 31 (2004)"},{"issue":"1","key":"24_CR11","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/2103621.2103709","volume":"47","author":"J Zhao","year":"2012","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M., Zdancewic, S.: Formalizing the LLVM intermediate representation for verified program transformations. SIGPLAN Not. 47(1), 427\u2013440 (2012). \n                      http:\/\/doi.acm.org\/10.1145\/2103621.2103709","journal-title":"SIGPLAN Not."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21668-3_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,22]],"date-time":"2019-07-22T20:16:03Z","timestamp":1563826563000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21668-3_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216676","9783319216683"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21668-3_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"14 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}