{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T19:42:24Z","timestamp":1779392544423,"version":"3.53.1"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,1,11]],"date-time":"2022-01-11T00:00:00Z","timestamp":1641859200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NWO","award":["016.Vidi.189.046"],"award-info":[{"award-number":["016.Vidi.189.046"]}]},{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,1,17]]},"DOI":"10.1145\/3497775.3503689","type":"proceedings-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T05:20:48Z","timestamp":1641964848000},"page":"100-115","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Mechanized verification of a fine-grained concurrent queue from meta\u2019s folly library"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4617-4976","authenticated-orcid":false,"given":"Simon Friis","family":"Vindum","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5864-7278","authenticated-orcid":false,"given":"Dan","family":"Frumin","sequence":"additional","affiliation":[{"name":"University of Groningen, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275499"},{"key":"e_1_3_2_1_2_1","unstructured":"Lars Birkedal and Ale\u0161 Bizjak. 2021. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic. https:\/\/iris-project.org\/tutorial-material.html  Lars Birkedal and Ale\u0161 Bizjak. 2021. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic. https:\/\/iris-project.org\/tutorial-material.html"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473586"},{"key":"e_1_3_2_1_4_1","unstructured":"Nathan Bronson. 2020. On the origins of the MPMC Queue. Personal Communication.  Nathan Bronson. 2020. On the origins of the MPMC Queue. Personal Communication."},{"key":"e_1_3_2_1_5_1","volume-title":"Distributed Data Store for the Social Graph. In 2013 USENIX Annual Technical Conference (USENIX ATC 13)","author":"Bronson Nathan","year":"2013","unstructured":"Nathan Bronson , Zach Amsden , George Cabrera , Prasad Chakka , Peter Dimov , Hui Ding , Jack Ferris , Anthony Giardullo , Sachin Kulkarni , Harry Li , Mark Marchukov , Dmitri Petrov , Lovro Puzar , Yee Jiun Song , and Venkat Venkataramani . 2013 . TAO: Facebook\u2019 s Distributed Data Store for the Social Graph. In 2013 USENIX Annual Technical Conference (USENIX ATC 13) . USENIX Association, San Jose, CA. 49\u201360. isbn:978-1-93 1971-01-0 https:\/\/www.usenix.org\/conference\/atc13\/technical-sessions\/presentation\/bronson Nathan Bronson, Zach Amsden, George Cabrera, Prasad Chakka, Peter Dimov, Hui Ding, Jack Ferris, Anthony Giardullo, Sachin Kulkarni, Harry Li, Mark Marchukov, Dmitri Petrov, Lovro Puzar, Yee Jiun Song, and Venkat Venkataramani. 2013. TAO: Facebook\u2019 s Distributed Data Store for the Social Graph. In 2013 USENIX Annual Technical Conference (USENIX ATC 13). USENIX Association, San Jose, CA. 49\u201360. isbn:978-1-931971-01-0 https:\/\/www.usenix.org\/conference\/atc13\/technical-sessions\/presentation\/bronson"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(1:20)2015"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.14279\/tuj.eceasst.66.889"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2796550"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.14279\/tuj.eceasst.53.792"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.021"},{"key":"e_1_3_2_1_14_1","volume-title":"Proceedings of Ottawa Linux Symposium. 85","author":"Franke Hubertus","year":"2002","unstructured":"Hubertus Franke , Rusty Russell , and Matthew Kirkwood . 2002 . Fuss, Futexes and Furwocks: Fast Userlevel Locking in Linux . In Proceedings of Ottawa Linux Symposium. 85 , 479\u2013495. Hubertus Franke, Rusty Russell, and Matthew Kirkwood. 2002. Fuss, Futexes and Furwocks: Fast Userlevel Locking in Linux. In Proceedings of Ottawa Linux Symposium. 85, 479\u2013495."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_3_2_1_16_1","volume-title":"ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. CoRR, abs\/2006.13635","author":"Frumin Dan","year":"2020","unstructured":"Dan Frumin , Robbert Krebbers , and Lars Birkedal . 2020. ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. CoRR, abs\/2006.13635 ( 2020 ), arxiv:2006.13635. arxiv:2006.13635 Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2020. ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. CoRR, abs\/2006.13635 (2020), arxiv:2006.13635. arxiv:2006.13635"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_3"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007912.1007944"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/32.2.98"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926417"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462189"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/103727.103729"},{"key":"e_1_3_2_1_32_1","volume-title":"Folly: Facebook Open-source Library. https:\/\/github.com\/facebook\/folly","year":"2021","unstructured":"Meta. 2021 . Folly: Facebook Open-source Library. https:\/\/github.com\/facebook\/folly Meta. 2021. Folly: Facebook Open-source Library. https:\/\/github.com\/facebook\/folly"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473571"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408978"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040326"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429111"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926415"},{"key":"e_1_3_2_1_45_1","volume-title":"Modular fine-grained concurrency verification. Ph. D. Dissertation","author":"Vafeiadis Viktor","unstructured":"Viktor Vafeiadis . 2008. Modular fine-grained concurrency verification. Ph. D. Dissertation . University of Cambridge . Viktor Vafeiadis. 2008. Modular fine-grained concurrency verification. Ph. D. Dissertation. University of Cambridge."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_18"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439930"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5770802"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359644"}],"event":{"name":"CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Philadelphia PA USA","acronym":"CPP '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3497775.3503689","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3497775.3503689","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:49:25Z","timestamp":1750193365000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3497775.3503689"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,11]]},"references-count":49,"alternative-id":["10.1145\/3497775.3503689","10.1145\/3497775"],"URL":"https:\/\/doi.org\/10.1145\/3497775.3503689","relation":{},"subject":[],"published":{"date-parts":[[2022,1,11]]},"assertion":[{"value":"2022-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}