{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T13:00:13Z","timestamp":1740142813998,"version":"3.37.3"},"reference-count":36,"publisher":"Oxford University Press (OUP)","license":[{"start":{"date-parts":[[2018,11,17]],"date-time":"2018-11-17T00:00:00Z","timestamp":1542412800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1093\/comjnl\/bxy116","type":"journal-article","created":{"date-parts":[[2018,11,8]],"date-time":"2018-11-08T07:33:12Z","timestamp":1541662392000},"source":"Crossref","is-referenced-by-count":0,"title":["Proving Linearizability Using Reduction"],"prefix":"10.1093","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2910-2214","authenticated-orcid":false,"given":"Tangliu","family":"Wen","sequence":"first","affiliation":[{"name":"State Key Laboratory of Software Engineering, School of Computer Science, Wuhan University, Wuhan, China"},{"name":"College of Applied Science, Jiangxi University of Science and Technology, Ganzhou, China"},{"name":"State International S&T Cooperation Base of Networked Supporting, Jiangxi Normal University, Nanchang, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lan","family":"Song","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Software Engineering, School of Computer Science, Wuhan University, Wuhan, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhen","family":"You","sequence":"additional","affiliation":[{"name":"State International S&T Cooperation Base of Networked Supporting, Jiangxi Normal University, Nanchang, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2018,11,17]]},"reference":[{"key":"key\n\t\t\t\t2019012511403083000_bxy116C1","doi-asserted-by":"crossref","first-page":"717","DOI":"10.1145\/361227.361234","article-title":"Reduction: a method of proving properties of parallel programs","volume":"18","author":"Lipton","year":"1975","journal-title":"Commun. ACM"},{"year":"2003","author":"Flanagan","key":"key\n\t\t\t\t2019012511403083000_bxy116C2"},{"key":"key\n\t\t\t\t2019012511403083000_bxy116C3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/640136.604176","article-title":"Types for atomicity","volume":"38","author":"Flanagan","year":"2003","journal-title":"ACM SIGPLAN Not."},{"key":"key\n\t\t\t\t2019012511403083000_bxy116C4","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1109\/TSE.2005.47","article-title":"Exploiting purity for atomicity","volume":"31","author":"Flanagan","year":"2005","journal-title":"IEEE Trans. Softw. Eng."},{"year":"2005","author":"Wang","key":"key\n\t\t\t\t2019012511403083000_bxy116C5"},{"key":"key\n\t\t\t\t2019012511403083000_bxy116C6","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1145\/78969.78972","article-title":"Linearizability: a correctness condition for concurrent objects","volume":"12","author":"Herlihy","year":"1990","journal-title":"ACM Trans. Program. Lang. Syst."},{"year":"2015","author":"Haas","key":"key\n\t\t\t\t2019012511403083000_bxy116C7"},{"year":"2004","author":"Hendler","key":"key\n\t\t\t\t2019012511403083000_bxy116C8"},{"year":"1996","author":"Michael","key":"key\n\t\t\t\t2019012511403083000_bxy116C9"},{"year":"2005","author":"Heller","key":"key\n\t\t\t\t2019012511403083000_bxy116C10"},{"year":"2009","author":"Qadeer","key":"key\n\t\t\t\t2019012511403083000_bxy116C11"},{"year":"2007","author":"Hoffman","key":"key\n\t\t\t\t2019012511403083000_bxy116C12"},{"year":"2004","author":"Michael","key":"key\n\t\t\t\t2019012511403083000_bxy116C13"},{"volume-title":"The Art of Multiprocessor Programming","year":"2008","author":"Herlihy","key":"key\n\t\t\t\t2019012511403083000_bxy116C14"},{"year":"2013","author":"Liang","key":"key\n\t\t\t\t2019012511403083000_bxy116C15"},{"year":"1988","author":"Cohen","key":"key\n\t\t\t\t2019012511403083000_bxy116C16"},{"year":"1989","author":"Back","key":"key\n\t\t\t\t2019012511403083000_bxy116C17"},{"year":"2008","author":"Groves","key":"key\n\t\t\t\t2019012511403083000_bxy116C18"},{"year":"2013","author":"Henzinger","key":"key\n\t\t\t\t2019012511403083000_bxy116C19"},{"key":"key\n\t\t\t\t2019012511403083000_bxy116C20","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/BF00289507","article-title":"Proof of correctness of data representation","volume":"1","author":"Hoare","year":"1972","journal-title":"Acta Informatica"},{"year":"2010","author":"O\u2019Hearn","key":"key\n\t\t\t\t2019012511403083000_bxy116C21"},{"year":"1986","author":"Treiber","key":"key\n\t\t\t\t2019012511403083000_bxy116C22"},{"year":"2017","author":"Khyzha","key":"key\n\t\t\t\t2019012511403083000_bxy116C23"},{"year":"2004","author":"Flanagan","key":"key\n\t\t\t\t2019012511403083000_bxy116C24"},{"key":"key\n\t\t\t\t2019012511403083000_bxy116C25","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1109\/TSE.2006.1599419","article-title":"Runtime analysis of atomicity for multithreaded programs","volume":"32","author":"Wang","year":"2006","journal-title":"IEEE Trans. Softw. Eng."},{"year":"2010","author":"Elmas","key":"key\n\t\t\t\t2019012511403083000_bxy116C26"},{"key":"key\n\t\t\t\t2019012511403083000_bxy116C27","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/1594834.1480885","article-title":"A calculus of atomic actions","volume":"44","author":"Elmas","year":"2009","journal-title":"ACM SIGPLAN Not."},{"year":"2016","author":"Singh","key":"key\n\t\t\t\t2019012511403083000_bxy116C28"},{"year":"2012","author":"Schellhorn","key":"key\n\t\t\t\t2019012511403083000_bxy116C29"},{"year":"2017","author":"Bouajjani","key":"key\n\t\t\t\t2019012511403083000_bxy116C30"},{"year":"2013","author":"Abdulla","key":"key\n\t\t\t\t2019012511403083000_bxy116C31"},{"year":"2016","author":"Abdulla","key":"key\n\t\t\t\t2019012511403083000_bxy116C32"},{"year":"2018","author":"Abdulla","key":"key\n\t\t\t\t2019012511403083000_bxy116C33"},{"year":"2008","author":"Vafeiadis","key":"key\n\t\t\t\t2019012511403083000_bxy116C34"},{"key":"key\n\t\t\t\t2019012511403083000_bxy116C35","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/s11784-012-0071-6","article-title":"How to write a 21st century proof","volume":"11","author":"Lamport","year":"2012","journal-title":"J. Fixed Point Theory Appl."},{"year":"2004","author":"Doherty","key":"key\n\t\t\t\t2019012511403083000_bxy116C36"}],"container-title":["The Computer Journal"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/comjnl\/advance-article-pdf\/doi\/10.1093\/comjnl\/bxy116\/26621163\/bxy116.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,31]],"date-time":"2019-10-31T22:38:52Z","timestamp":1572561532000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/comjnl\/advance-article\/doi\/10.1093\/comjnl\/bxy116\/5187914"}},"subtitle":[],"editor":[{"given":"Domenico","family":"Rosaci","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]}],"short-title":[],"issued":{"date-parts":[[2018,11,17]]},"references-count":36,"URL":"https:\/\/doi.org\/10.1093\/comjnl\/bxy116","relation":{},"ISSN":["0010-4620","1460-2067"],"issn-type":[{"type":"print","value":"0010-4620"},{"type":"electronic","value":"1460-2067"}],"subject":[],"published":{"date-parts":[[2018,11,17]]}}}