{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,5]],"date-time":"2026-05-05T04:16:50Z","timestamp":1777954610688,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,7,16]]},"DOI":"10.1145\/3694906.3743304","type":"proceedings-article","created":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T16:19:56Z","timestamp":1752682796000},"page":"540-554","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Machine-Verification of MemSnap: An Efficient, Far-Future Linearizable Snapshot Algorithm"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2681-1632","authenticated-orcid":false,"given":"Siddhartha","family":"Jayanti","sequence":"first","affiliation":[{"name":"Dartmouth College, Hanover, NH, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6218-2466","authenticated-orcid":false,"given":"Ugur Y.","family":"Yavuz","sequence":"additional","affiliation":[{"name":"Boston University, Boston, MA, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,7,16]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/153724.153741"},{"key":"e_1_3_2_2_3_1","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"1","volume-title":"38th International Symposium on Distributed Computing (DISC 2024) (Dagstuhl","author":"Bashari B.","year":"2024","unstructured":"Bashari, B., Chan, D. Y. C., and Woelfel, P. A fully concurrent adaptive snapshot object for RMWable shared-memory. In 38th International Symposium on Distributed Computing (DISC 2024) (Dagstuhl, Germany, 2024), D. Alistarh, Ed., vol. 319 of Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl -- Leibniz-Zentrum f\u00fcr Informatik, pp. 7:1--7:22."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3465084.3467939"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473586"},{"key":"e_1_3_2_2_6_1","volume-title":"GitHub repository. Url: https:\/\/github.com\/cmuparlay\/parlayhash","author":"Parlay","year":"2024","unstructured":"CMUParlay. ParlayHash. GitHub repository. Url: https:\/\/github.com\/cmuparlay\/parlayhash, 2024."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_14"},{"key":"e_1_3_2_2_8_1","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"1","volume-title":"31st European Conference on Object-Oriented Programming (ECOOP 2017) (Dagstuhl","author":"Delbianco G. A.","year":"2017","unstructured":"Delbianco, G. A., Sergey, I., Nanevski, A., and Banerjee, A. Concurrent data structures linked in time. In 31st European Conference on Object-Oriented Programming (ECOOP 2017) (Dagstuhl, Germany, 2017), P. M\u00fcller, Ed., vol. 74 of Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl -- Leibniz-Zentrum f\u00fcr Informatik, pp. 8:1--8:30."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2796550"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993636.1993687"},{"key":"e_1_3_2_2_11_1","volume-title":"The Graph Mining Library. GitHub repository. Url: https:\/\/github.com\/google\/graph-mining","author":"Google Graph Mining","year":"2023","unstructured":"Google Graph Mining team. The Graph Mining Library. GitHub repository. Url: https:\/\/github.com\/google\/graph-mining, 2023."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_18"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4705416"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/571825.571875"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1060590.1060697"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3732772.3733542"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3662158.3662820"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3670684.3673406"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632924"},{"key":"e_1_3_2_2_21_1","first-page":"142","article-title":"A simple technique for machine-verifying lock-free data structures","author":"Jayanti S.","year":"2024","unstructured":"Jayanti, S. Possibility tracking: A simple technique for machine-verifying lock-free data structures. Bull. EATCS 142 (2024).","journal-title":"Bull. EATCS"},{"key":"e_1_3_2_2_22_1","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"1","volume-title":"35th International Symposium on Distributed Computing (DISC 2021) (Dagstuhl","author":"Jayanti S.","year":"2021","unstructured":"Jayanti, S., and Shun, J. Fast arrays: Atomic arrays with constant time initialization. In 35th International Symposium on Distributed Computing (DISC 2021) (Dagstuhl, Germany, 2021), S. Gilbert, Ed., vol. 209 of Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl -- Leibniz-Zentrum f\u00fcr Informatik, pp. 25:1--25:19."},{"key":"e_1_3_2_2_23_1","unstructured":"Jayanti S. V. Simple Fast Scalable and Reliable Multiprocessor Algorithms. PhD thesis MIT USA 2023."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933057.2933108"},{"key":"e_1_3_2_2_25_1","unstructured":"Jensen E. H. Hagensen G. W. and Broughton J. M. A new approach to exclusive data access in shared memory multiprocessors. Tech. Rep. UCRL-97663 Lawrence Livermore National Laboratory 1987."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/91930.91950"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_24"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_2_31_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport L.","year":"2002","unstructured":"Lamport, L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, June 2002."},{"key":"e_1_3_2_2_32_1","volume-title":"May","author":"Lamport L.","year":"2017","unstructured":"Lamport, L., and Merz, S. Auxiliary variables in TLA+, May 2017."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3492545"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1993.274940"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_3_2_2_36_1","first-page":"401","volume-title":"Eds. Springer Berlin Heidelberg","author":"Merz S.","year":"2008","unstructured":"Merz, S. The specification language TLA+. In Logics of Specification Languages, D. Bj\u00f8rner and M. C. Henson, Eds. Springer Berlin Heidelberg, Berlin, Heidelberg, 2008, pp. 401--451."},{"key":"e_1_3_2_2_37_1","volume-title":"Proc. ACM Program. Lang. 6, POPL (Jan.","author":"\u00d6hman J.","year":"2022","unstructured":"\u00d6hman, J., and Nanevski, A. Visibility reasoning for concurrent snapshot algorithms. Proc. ACM Program. Lang. 6, POPL (Jan. 2022)."},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571231"},{"key":"e_1_3_2_2_39_1","volume-title":"Software bug contributed to blackout. Security Focus","author":"Poulsen K.","year":"2004","unstructured":"Poulsen, K. Software bug contributed to blackout. Security Focus (2004)."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629496"},{"key":"e_1_3_2_2_41_1","unstructured":"Vafeiadis V. Modular fine-grained concurrency verification. Tech. Rep. UCAM-CL-TR-726 University of Cambridge Computer Laboratory July 2008."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437801.3441602"}],"event":{"name":"SPAA '25: 37th ACM Symposium on Parallelism in Algorithms and Architectures","location":"Portland OR USA","acronym":"SPAA '25","sponsor":["SIGACT ACM Special Interest Group on Algorithms and Computation Theory","SIGARCH ACM Special Interest Group on Computer Architecture","EATCS European Association for Theoretical Computer Science"]},"container-title":["Proceedings of the 37th ACM Symposium on Parallelism in Algorithms and Architectures"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3694906.3743304","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T19:20:24Z","timestamp":1777922424000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3694906.3743304"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,16]]},"references-count":42,"alternative-id":["10.1145\/3694906.3743304","10.1145\/3694906"],"URL":"https:\/\/doi.org\/10.1145\/3694906.3743304","relation":{},"subject":[],"published":{"date-parts":[[2025,7,16]]},"assertion":[{"value":"2025-07-16","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}