{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:56:57Z","timestamp":1774025817596,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642150562","type":"print"},{"value":"9783642150579","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15057-9_4","type":"book-chapter","created":{"date-parts":[[2010,8,11]],"date-time":"2010-08-11T07:01:15Z","timestamp":1281510075000},"page":"55-70","source":"Crossref","is-referenced-by-count":26,"title":["A Rely-Guarantee Proof System for x86-TSO"],"prefix":"10.1007","author":[{"given":"Tom","family":"Ridge","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. CoRR, abs\/0901.3619 (2009)","DOI":"10.1007\/s10817-009-9148-3"},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/BF00288686","volume":"1","author":"M. Clint","year":"1972","unstructured":"Clint, M., Hoare, C.A.R.: Program proving: Jumps and functions. Acta Informatica\u00a01, 214\u2013224 (1972)","journal-title":"Acta Informatica"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-540-87873-5_14","volume-title":"Verified Software: Theories, Tools, Experiments","author":"J.W. Coleman","year":"2008","unstructured":"Coleman, J.W.: Expression decomposition in a Rely\/Guarantee context. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 146\u2013160. Springer, Heidelberg (2008)"},{"key":"4_CR4","unstructured":"Cohen, E., Schirmer, N.: A better reduction theorem for store buffers. Technical report (2009)"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proc.\u00a0American Mathematical Society Symposia in Applied Mathematics, vol.\u00a019 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-540-45236-2_15","volume-title":"FME 2003: Formal Methods","author":"N. Henderson","year":"2003","unstructured":"Henderson, N.: Proving the correctness of Simpson\u2019s 4-slot ACM using an assertional Rely-Guarantee proof method. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 244\u2013263. Springer, Heidelberg (2003)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Hoare: An axiomatic basis for computer programming. CACM: Communications of the ACM\u00a012 (1969)","DOI":"10.1145\/363235.363259"},{"key":"4_CR8","unstructured":"Jones, C.B.: Development Methods for Computer Programmes Including a Notion of Interference. PhD thesis, Prgr. Res. Grp. 25, Oxford Univ., Comp. Lab., UK (June 1981)"},{"key":"4_CR9","unstructured":"Linux Kernel mailing list, thread \u201cspin_unlock optimization(i386)\u201d, 119 messages (November 20 - December 7, 1999), http:\/\/www.gossamer-threads.com\/lists\/engine?post=105365;list=linux (Accessed 2009\/11\/18)"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Myreen, M.O., Slind, K., Gordon, M.J.C.: Machine-code verification for multiple architectures: An application of decompilation into logic. In: Proc. FMCAD (2008)","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/978-3-642-03359-9_27","volume-title":"TPHOLs 2009","author":"S. Owens","year":"2009","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 391\u2013407. Springer, Heidelberg (2009)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"478","DOI":"10.1007\/978-3-642-14107-2_23","volume-title":"ECOOP 2010","author":"S. Owens","year":"2010","unstructured":"Owens, S.: Reasoning about the implementation of concurrency abstractions on x86-TSO. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 478\u2013503. Springer, Heidelberg (2010)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Park, Dill: An executable specification, analyzer and verifier for RMO (relaxed memory order). In: SPAA: Annual ACM Symposium on Parallel Algorithms and Architectures (1995)","DOI":"10.1145\/215399.215413"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-74591-4_21","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Ridge","year":"2007","unstructured":"Ridge, T.: Operational reasoning for concurrent Caml programs and weak memory models. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 278\u2013293. Springer, Heidelberg (2007)"},{"key":"4_CR15","unstructured":"Rushby, J.: Model checking Simpson\u2019s four-slot fully asynchronous communication mechanism (2002)"},{"issue":"1","key":"4_CR16","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1049\/ip-e.1990.0002","volume":"137","author":"H.R. Simpson","year":"1990","unstructured":"Simpson, H.R.: Four-slot fully asynchronous communication mechanism. IEE Proceedings, Computers and Digital Techniques\u00a0137(1), 17\u201330 (1990)","journal-title":"IEE Proceedings, Computers and Digital Techniques"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15057-9_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,4]],"date-time":"2021-11-04T15:53:38Z","timestamp":1636041218000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15057-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642150562","9783642150579"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15057-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}