{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:38Z","timestamp":1751660498723,"version":"3.28.0"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2006,3,29]]},"DOI":"10.1145\/1122971.1122992","type":"proceedings-article","created":{"date-parts":[[2006,5,8]],"date-time":"2006-05-08T21:40:43Z","timestamp":1147124443000},"page":"129-136","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":65,"title":["Proving correctness of highly-concurrent linearisable objects"],"prefix":"10.1145","author":[{"given":"Viktor","family":"Vafeiadis","sequence":"first","affiliation":[{"name":"University of Cambridge"}]},{"given":"Maurice","family":"Herlihy","sequence":"additional","affiliation":[{"name":"Brown University"}]},{"given":"Tony","family":"Hoare","sequence":"additional","affiliation":[{"name":"Microsoft Research Cambridge"}]},{"given":"Marc","family":"Shapiro","sequence":"additional","affiliation":[{"name":"INRIA Rocquencourt & LIP6"}]}],"member":"320","published-online":{"date-parts":[[2006,3,29]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/203095.201069"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00263762"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/776816.776834"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30232-2_7"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.12.006"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-004-0115-2"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359666"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/645958.676105"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11795490_3"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/647767.733780"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_1_12_1","volume-title":"W. on Specification and Verification of Component-Based Systems","author":"Jacobs B.","year":"2004","unstructured":"B. Jacobs , K. R. M. Leino , and W. Schulte . Verification of multithreaded object-oriented programs with invariants . In W. on Specification and Verification of Component-Based Systems , Oct. 2004 .]] B. Jacobs, K. R. M. Leino, and W. Schulte. Verification of multithreaded object-oriented programs with invariants. In W. on Specification and Verification of Component-Based Systems, Oct. 2004.]]"},{"key":"e_1_3_2_1_13_1","first-page":"321","volume-title":"IFIP Congress","author":"Jones C. B.","year":"1983","unstructured":"C. B. Jones . Specification and design of (parallel) programs . In IFIP Congress , pages 321 -- 332 , 1983 .]] C. B. Jones. Specification and design of (parallel) programs. In IFIP Congress, pages 321--332, 1983.]]"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_1_15_1","volume-title":"Proc. COMPOS'97 Symp.","volume":"1536","author":"Lamport L.","year":"1997","unstructured":"L. Lamport . Composition : A way to make proofs harder . In Proc. COMPOS'97 Symp. , volume 1536 of Lecture Notes in Computer Science, pages 402--423. Springer-Verlag , 1997 .]] L. Lamport. Composition: A way to make proofs harder. In Proc. COMPOS'97 Symp., volume 1536 of Lecture Notes in Computer Science, pages 402--423. Springer-Verlag, 1997.]]"},{"key":"e_1_3_2_1_16_1","unstructured":"D. Lea. Concurrent hash map in JSR166 concurrency utilities. http:\/\/gee.cs.oswego.edu\/dl\/concurrency-interest\/.]]  D. Lea. Concurrent hash map in JSR166 concurrency utilities. http:\/\/gee.cs.oswego.edu\/dl\/concurrency-interest\/.]]"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/41840.41852"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/564870.564881"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1006\/jpdc.1998.1446"},{"key":"e_1_3_2_1_20_1","first-page":"49","volume-title":"CONCUR","author":"O'Hearn P. W.","year":"2004","unstructured":"P. W. O'Hearn . Resources, concurrency and local reasoning . In CONCUR , pages 49 -- 67 , 2004 .]] P. W. O'Hearn. Resources, concurrency and local reasoning. In CONCUR, pages 49--67, 2004.]]"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"}],"event":{"name":"PPoPP06: ACM SIGPLAN 2006 Symposium on Principles and Practice of Parallel Programming 2006","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"],"location":"New York New York USA","acronym":"PPoPP06"},"container-title":["Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1122971.1122992","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T10:54:41Z","timestamp":1673434481000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1122971.1122992"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,3,29]]},"references-count":21,"alternative-id":["10.1145\/1122971.1122992","10.1145\/1122971"],"URL":"https:\/\/doi.org\/10.1145\/1122971.1122992","relation":{},"subject":[],"published":{"date-parts":[[2006,3,29]]},"assertion":[{"value":"2006-03-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}