{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:49:57Z","timestamp":1775868597790,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":84,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,6,11]],"date-time":"2020-06-11T00:00:00Z","timestamp":1591833600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100014718","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1925605, CCF-1618059, CCF-181563"],"award-info":[{"award-number":["1925605, CCF-1618059, CCF-181563"]}],"id":[{"id":"10.13039\/100014718","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,6,11]]},"DOI":"10.1145\/3385412.3386029","type":"proceedings-article","created":{"date-parts":[[2020,6,7]],"date-time":"2020-06-07T01:40:10Z","timestamp":1591494010000},"page":"181-196","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Verifying concurrent search structure templates"],"prefix":"10.1145","author":[{"given":"Siddharth","family":"Krishna","sequence":"first","affiliation":[{"name":"Microsoft Research, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nisarg","family":"Patel","sequence":"additional","affiliation":[{"name":"New York University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dennis","family":"Shasha","sequence":"additional","affiliation":[{"name":"New York University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[{"name":"New York University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,6,11]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Parosh Aziz Abdulla Fr\u00e9d\u00e9ric Haziza Luk\u00e1s Hol\u00edk Bengt Jonsson and Ahmed Rezine. 2013."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_23"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_16"},{"key":"e_1_3_2_1_4_1","volume-title":"19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings (Lecture Notes in Computer Science), Werner Damm and Holger Hermanns (Eds.)","volume":"4590","author":"Amit Daphna","year":"2007","unstructured":"Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, and Eran Yahav. 2007. Comparison Under Abstraction for Verifying Linearizability. In Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings (Lecture Notes in Computer Science), Werner Damm and Holger Hermanns (Eds.), Vol. 4590."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","unstructured":"Springer 477\u2013490. 10.1007\/978-3-540-73368-3_49","DOI":"10.1007\/978-3-540-73368-3_49"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_6"},{"key":"e_1_3_2_1_7_1","unstructured":"Ales Bizjak Daniel Gratzer Robbert Krebbers and Lars Birkedal. 2019."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290378"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.059"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_17"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_8"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_28"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_3_2_1_16_1","unstructured":"Pavol Cern\u00fd Arjun Radhakrishna Damien Zufferey Swarat Chaudhuri and Rajeev Alur. 2010."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_41"},{"key":"e_1_3_2_1_18_1","volume-title":"Aspect-oriented linearizability proofs. Logical Methods in Computer Science 11, 1","author":"Chakraborty Soham","year":"2015","unstructured":"Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. 2015. Aspect-oriented linearizability proofs. Logical Methods in Computer Science 11, 1 (2015)."},{"key":"e_1_3_2_1_19_1","volume-title":"Wheelhouse","author":"da Rocha Pinto Pedro","year":"2011","unstructured":"Pedro da Rocha Pinto, Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, and Mark J. Wheelhouse. 2011."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048131"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.8"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726"},{"key":"e_1_3_2_1_26_1","unstructured":"2676963"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2818638"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_11"},{"key":"e_1_3_2_1_29_1","unstructured":"Yotam M. Y. Feldman Constantin Enea Adam Morrison Noam Rinetzky and Sharon Shoham. 2018."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.DISC.2018.23"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_13"},{"key":"e_1_3_2_1_32_1","unstructured":"Ivana Filipovic Peter W. O\u2019Hearn Noam Rinetzky and Hongseok Yang. 2009."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_19"},{"key":"e_1_3_2_1_34_1","unstructured":"Dan Frumin Robbert Krebbers and Lars Birkedal. 2018."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_3_2_1_36_1","unstructured":"Ming Fu Yong Li Xinyu Feng Zhong Shao and Yu Zhang. 2010."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_27"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45414-4_21"},{"key":"e_1_3_2_1_40_1","volume-title":"Wing","author":"Herlihy Maurice","year":"1990","unstructured":"Maurice Herlihy and Jeannette M. Wing. 1990."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_1_42_1","volume-title":"14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings (Lecture Notes in Computer Science), Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni (Eds.)","volume":"7737","author":"Heule Stefan","unstructured":"Stefan Heule, K. Rustan M. Leino, Peter M\u00fcller, and Alexander J. Summers. 2013. Abstract Read Permissions: Fractional Permissions without the Fractions. In Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings (Lecture Notes in Computer Science), Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni (Eds.), Vol. 7737."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","unstructured":"Springer 315\u2013334. 10.1007\/978-3-642-35873-9_20","DOI":"10.1007\/978-3-642-35873-9_20"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235"},{"key":"e_1_3_2_1_45_1","unstructured":"363259"},{"key":"e_1_3_2_1_46_1","volume-title":"Proceedings of the IFIP 9th World Computer Congress","author":"Jones Cliff B.","year":"1983","unstructured":"Cliff B. Jones. 1983. Specification and Design of (Parallel) Programs. In Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983, R. E. A. Mason (Ed.). North-Holland\/IFIP, 321\u2013332."},{"key":"e_1_3_2_1_47_1","unstructured":"Ralf Jung Robbert Krebbers Lars Birkedal and Derek Dreyer. 2016."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913"},{"key":"e_1_3_2_1_49_1","unstructured":"2951943"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_24"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158125"},{"key":"e_1_3_2_1_56_1","unstructured":"Siddharth Krishna Alexander J. Summers and Thomas Wies. 2020."},{"key":"e_1_3_2_1_57_1","volume-title":"ESOP 2020, as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020","author":"Global Graph Properties Local Reasoning","year":"2020","unstructured":"Local Reasoning for Global Graph Properties. Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 (2020). To appear."},{"key":"e_1_3_2_1_58_1","volume-title":"Levandoski and Sudipta Sengupta","author":"Justin","year":"2013","unstructured":"Justin J. Levandoski and Sudipta Sengupta. 2013."},{"key":"e_1_3_2_1_59_1","volume-title":"A Latch-Free B-Tree for Log-Structured Flash Storage","author":"Tree The","year":"2013","unstructured":"The BW-Tree: A Latch-Free B-Tree for Log-Structured Flash Storage. IEEE Data Eng. Bull. 36, 2 (2013), 56\u201362. http:\/\/sites.computer.org\/debull\/A13june\/ bwtree1.pdf"},{"key":"e_1_3_2_1_60_1","unstructured":"Hongjin Liang and Xinyu Feng. 2013."},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956"},{"key":"e_1_3_2_1_62_1","unstructured":"2462189"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706329"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290371"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_3_2_1_67_1","volume-title":"15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings (Lecture Notes in Computer Science), Laurent Fribourg (Ed.)","volume":"2142","author":"O\u2019Hearn Peter W.","year":"2001","unstructured":"Peter W. O\u2019Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures. In Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings (Lecture Notes in Computer Science), Laurent Fribourg (Ed.), Vol. 2142."},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","unstructured":"Springer 1\u201319. 10.1007\/3-540-44802-0_1","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_2_1_69_1","unstructured":"Peter W. O\u2019Hearn Noam Rinetzky Martin T. Vechev Eran Yahav and Greta Yorsh. 2010."},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/1835698.1835722"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_54"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_9"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_29"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2983999"},{"key":"e_1_3_2_1_78_1","volume-title":"Shasha and Nathan Goodman","author":"Dennis","year":"1988","unstructured":"Dennis E. Shasha and Nathan Goodman. 1988."},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/42201.42204"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_27"},{"key":"e_1_3_2_1_82_1","volume-title":"Parkinson","author":"Vafeiadis Viktor","year":"2007","unstructured":"Viktor Vafeiadis and Matthew J. Parkinson. 2007. A Marriage of Rely\/Guarantee and Separation Logic. In CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings (Lecture Notes in Computer Science), Lu\u00eds Caires and Vasco Thudichum Vasconcelos (Eds.), Vol. 4703."},{"key":"e_1_3_2_1_83_1","doi-asserted-by":"publisher","unstructured":"Springer 256\u2013271. 10.1007\/978-3-540-74407-8_18","DOI":"10.1007\/978-3-540-74407-8_18"},{"key":"e_1_3_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_36"}],"event":{"name":"PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"London UK","acronym":"PLDI '20","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3386029","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3385412.3386029","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:38:49Z","timestamp":1750199929000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3386029"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,11]]},"references-count":84,"alternative-id":["10.1145\/3385412.3386029","10.1145\/3385412"],"URL":"https:\/\/doi.org\/10.1145\/3385412.3386029","relation":{},"subject":[],"published":{"date-parts":[[2020,6,11]]},"assertion":[{"value":"2020-06-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}