{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:11:24Z","timestamp":1750306284648,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":13,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,4,4]],"date-time":"2016-04-04T00:00:00Z","timestamp":1459728000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,4,4]]},"DOI":"10.1145\/2851613.2851837","type":"proceedings-article","created":{"date-parts":[[2016,6,2]],"date-time":"2016-06-02T19:23:42Z","timestamp":1464895422000},"page":"1694-1699","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Invariant generation for linearizability proofs"],"prefix":"10.1145","author":[{"given":"Graeme","family":"Smith","sequence":"first","affiliation":[{"name":"The University of Queensland, Australia"}]},{"given":"John","family":"Derrick","sequence":"additional","affiliation":[{"name":"University of Sheffield, UK"}]}],"member":"320","published-online":{"date-parts":[[2016,4,4]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","unstructured":"D. Amit N. Rinetzky T. Reps M. Sagiv and E. Yahav. Comparison under abstraction for verifying linearizability. In W. Damm and H. Hermanns editors CAV 2007 volume 4590 of LNCS pages 477--490. Springer 2007.","DOI":"10.5555\/1770351.1770417"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","unstructured":"C. Calcagno M. Parkinson and V. Vafeiadis. Modular safety checking for fine-grained concurrency. In H. Nielson and G. Fil\u00e9 editors SAS 2007 volume 4634 of LNCS pages 233--238. Springer 2007.","DOI":"10.5555\/2391451.2391468"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","unstructured":"J. Derrick G. Schellhorn and H. Wehrheim. Proving linearizability via non-atomic refinement. In J. Davies and J. Gibbons editors IFM 2007 volume 4591 of LNCS pages 195--214. Springer 2007.","DOI":"10.5555\/1770498.1770509"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1889997.1890001"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","unstructured":"J. Derrick G. Schellhorn and H. Wehrheim. Verifying linearisabilty with potential linearisation points. In M. Butler and W. Schulte editors FM 2011 volume 6664 of LNCS pages 323--337. Springer 2011.","DOI":"10.5555\/2021296.2021331"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10181-1_21"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"S. Doherty L. Groves V. Luchangco and M. Moir. Formal verification of a practical lock-free queue algorithm. In D. de Frutos-Escrig and M. Nunez editors FORTE 2004 volume 3235 of LNCS pages 97--114. Springer 2004.","DOI":"10.1007\/978-3-540-30232-2_7"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007912.1007944"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0435-9_1"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629496"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1122971.1122992"}],"event":{"name":"SAC 2016: Symposium on Applied Computing","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"],"location":"Pisa Italy","acronym":"SAC 2016"},"container-title":["Proceedings of the 31st Annual ACM Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2851613.2851837","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2851613.2851837","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:38:57Z","timestamp":1750221537000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2851613.2851837"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4,4]]},"references-count":13,"alternative-id":["10.1145\/2851613.2851837","10.1145\/2851613"],"URL":"https:\/\/doi.org\/10.1145\/2851613.2851837","relation":{},"subject":[],"published":{"date-parts":[[2016,4,4]]},"assertion":[{"value":"2016-04-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}