{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:16:15Z","timestamp":1760044575473,"version":"3.41.0"},"reference-count":92,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2127309, 1837030"],"award-info":[{"award-number":["2127309, 1837030"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>Verification of distributed systems using systematic exploration is daunting because of the many possible interleavings of messages and failures.  \nWhen faced with this scalability challenge, existing approaches have traditionally mitigated state space explosion by avoiding exploration of redundant states (e.g., via state hashing) and redundant interleavings of transitions (e.g., via partial-order reductions).  \nIn this paper, we present an efficient symbolic exploration method that not only avoids redundancies in states and interleavings, but additionally  \navoids redundant computations that are performed during updates to states on transitions.  \nOur symbolic explorer leverages a novel, fine-grained, canonical representation of distributed system configurations (states) to identify opportunities for avoiding such redundancies on-the-fly.  \nThe explorer also includes an interface that is compatible with abstractions for state-space reduction and with partial-order and other reductions for avoiding redundant interleavings.  \nWe implement our approach in the tool Psym and empirically demonstrate that it outperforms a state-of-the-art exploration tool, can successfully verify many common distributed protocols, and can scale to multiple real-world industrial case studies across<\/jats:p>","DOI":"10.1145\/3591247","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"660-685","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Psym: Efficient Symbolic Exploration of Distributed Systems"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1605-5383","authenticated-orcid":false,"given":"Lauren","family":"Pick","sequence":"first","affiliation":[{"name":"University of California at Berkeley, USA \/ University of Wisconsin-Madison, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9006-0100","authenticated-orcid":false,"given":"Ankush","family":"Desai","sequence":"additional","affiliation":[{"name":"Amazon Web Services, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6676-9400","authenticated-orcid":false,"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/7929"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/s095679689700261x"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_28"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_42"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_14"},{"key":"e_1_2_1_7_1","volume-title":"Handbook of Satisfiability (Frontiers in Artificial Intelligence and Applications","volume":"885","author":"Barrett Clark W.","year":"2009","unstructured":"Clark W. Barrett , Roberto Sebastiani , Sanjit A. Seshia , and Cesare Tinelli . 2009 . Satisfiability Modulo Theories . In Handbook of Satisfiability (Frontiers in Artificial Intelligence and Applications , Vol. 185). IOS Press, 825\u2013 885 . Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. 2009. Satisfiability Modulo Theories. In Handbook of Satisfiability (Frontiers in Artificial Intelligence and Applications, Vol. 185). IOS Press, 825\u2013885."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/800221.806707"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88885-5_10"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_13_1","volume-title":"Engler","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson R . Engler . 2008 . KLEE : Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In OSDI. USENIX Association , 209\u2013224. Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In OSDI. USENIX Association, 209\u2013224."},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Sagar Chaki and Arie Gurfinkel. 2018. BDD-Based Symbolic Model Checking. In Handbook of Model Checking. 219\u2013245. \t\t\t\t  Sagar Chaki and Arie Gurfinkel. 2018. BDD-Based Symbolic Model Checking. In Handbook of Model Checking. 219\u2013245.","DOI":"10.1007\/978-3-319-10575-8_8"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3419614.3423256"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359108"},{"key":"e_1_2_1_17_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"2001","unstructured":"Edmund M. Clarke , Orna Grumberg , and Doron A . Peled . 2001 . Model checking. MIT Press . Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 2001. Model checking. MIT Press."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737996"},{"key":"e_1_2_1_21_1","unstructured":"Murat Demirbas. 2017. https:\/\/github.com\/muratdem\/HLC \t\t\t\t  Murat Demirbas. 2017. https:\/\/github.com\/muratdem\/HLC"},{"key":"e_1_2_1_22_1","unstructured":"Murat Demirbas. 2017. https:\/\/github.com\/muratdem\/PlusCal-examples\/blob\/master\/2PCTM\/2PCwithBTM.tla \t\t\t\t  Murat Demirbas. 2017. https:\/\/github.com\/muratdem\/PlusCal-examples\/blob\/master\/2PCTM\/2PCwithBTM.tla"},{"key":"e_1_2_1_23_1","unstructured":"Murat Demirbas. 2017. TLA+\/Pluscal modeling of 2-phase commit transactions. http:\/\/muratbuffalo.blogspot.com\/2017\/12\/tlapluscal-modeling-of-2-phase-commit.html \t\t\t\t  Murat Demirbas. 2017. TLA+\/Pluscal modeling of 2-phase commit transactions. http:\/\/muratbuffalo.blogspot.com\/2017\/12\/tlapluscal-modeling-of-2-phase-commit.html"},{"key":"e_1_2_1_24_1","unstructured":"Murat Demirbas. 2019. The Ben-Or decentralized consensus algorithm. https:\/\/muratbuffalo.blogspot.com\/2019\/12\/the-ben-or-decentralized-consensus.html \t\t\t\t  Murat Demirbas. 2019. The Ben-Or decentralized consensus algorithm. https:\/\/muratbuffalo.blogspot.com\/2019\/12\/the-ben-or-decentralized-consensus.html"},{"key":"e_1_2_1_25_1","unstructured":"Ankush Desai. 2022. Formal Modeling and Analysis of Distributed Systems. https:\/\/www.youtube.com\/watch?v=5YjsSDDWFDY \t\t\t\t  Ankush Desai. 2022. Formal Modeling and Analysis of Distributed Systems. https:\/\/www.youtube.com\/watch?v=5YjsSDDWFDY"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660211"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462184"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462184"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276529"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786861"},{"key":"e_1_2_1_31_1","volume-title":"Amazon S3 Strong Consistency. https:\/\/www.twitch.tv\/videos\/962963706?t=0h15m15s [Online","author":"Desai Ankush","year":"2022","unstructured":"Ankush Desai , Serdar Tasiran , and Vishwas Narenda . 2021. Amazon S3 Strong Consistency. https:\/\/www.twitch.tv\/videos\/962963706?t=0h15m15s [Online ; accessed 2022 ]. Ankush Desai, Serdar Tasiran, and Vishwas Narenda. 2021. Amazon S3 Strong Consistency. https:\/\/www.twitch.tv\/videos\/962963706?t=0h15m15s [Online; accessed 2022]."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18070-5_2"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491453"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_3"},{"key":"e_1_2_1_37_1","volume-title":"P Case Studies. https:\/\/p-org.github.io\/P\/casestudies\/ [Online","author":"GitHub P","year":"2021","unstructured":"P GitHub . 2021. P Case Studies. https:\/\/p-org.github.io\/P\/casestudies\/ [Online ; accessed 2021 ]. P GitHub. 2021. P Case Studies. https:\/\/p-org.github.io\/P\/casestudies\/ [Online; accessed 2021]."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0023731"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1132863.1132867"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_46_1","first-page":"1","article-title":"Flexible Paxos: Quorum Intersection Revisited. In OPODIS (LIPIcs, Vol. 70)","volume":"25","author":"Howard Heidi","year":"2016","unstructured":"Heidi Howard , Dahlia Malkhi , and Alexander Spiegelman . 2016 . Flexible Paxos: Quorum Intersection Revisited. In OPODIS (LIPIcs, Vol. 70) . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik , 25 : 1 \u2013 25 :14. Heidi Howard, Dahlia Malkhi, and Alexander Spiegelman. 2016. Flexible Paxos: Quorum Intersection Revisited. In OPODIS (LIPIcs, Vol. 70). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 25:1\u201325:14.","journal-title":"Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik"},{"key":"e_1_2_1_47_1","unstructured":"Heidi Howard Dahlia Malkhi and Alexander Spiegelman. 2022. TLA+ Specification of Flexible Paxos. https:\/\/github.com\/fpaxos\/fpaxos-tlaplus \t\t\t\t  Heidi Howard Dahlia Malkhi and Alexander Spiegelman. 2022. TLA+ Specification of Flexible Paxos. https:\/\/github.com\/fpaxos\/fpaxos-tlaplus"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46017-9_5"},{"key":"e_1_2_1_49_1","unstructured":"Jepsen. 2021. Jepsen Tool. https:\/\/jepsen.io\/ \t\t\t\t  Jepsen. 2021. Jepsen Tool. https:\/\/jepsen.io\/"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_31"},{"key":"e_1_2_1_52_1","volume-title":"Symposium on Networked Systems Design and Implementation.","author":"Killian Charles Edwin","year":"2007","unstructured":"Charles Edwin Killian , James W. Anderson , Ranjit Jhala , and Amin Vahdat . 2007 . Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code . In Symposium on Networked Systems Design and Implementation. Charles Edwin Killian, James W. Anderson, Ranjit Jhala, and Amin Vahdat. 2007. Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code. In Symposium on Networked Systems Design and Implementation."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360549"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-14472-6_2"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254088"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_36"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_7"},{"key":"e_1_2_1_58_1","article-title":"Paxos Made Simple","volume":"32","author":"Lamport Leslie","year":"2001","unstructured":"Leslie Lamport . 2001 . Paxos Made Simple . ACM SIGACT News , 32 , 4 (2001), Dec. . Leslie Lamport. 2001. Paxos Made Simple. ACM SIGACT News, 32, 4 (2001), Dec..","journal-title":"ACM SIGACT News"},{"volume-title":"The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","key":"e_1_2_1_59_1","unstructured":"Leslie Lamport . 2002. Specifying Systems , The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley . Leslie Lamport. 2002. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley."},{"volume-title":"Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation (OSDI).","author":"Leesatapornwongsa Tanakorn","key":"e_1_2_1_60_1","unstructured":"Tanakorn Leesatapornwongsa , Mingzhe Hao , Pallavi Joshi , Jeffrey F. Lukman , and Haryadi S. Gunawi . 2014. SAMC: Semantic-aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems . In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation (OSDI). Tanakorn Leesatapornwongsa, Mingzhe Hao, Pallavi Joshi, Jeffrey F. Lukman, and Haryadi S. Gunawi. 2014. SAMC: Semantic-aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems. In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation (OSDI)."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_22"},{"volume-title":"Distributed Algorithms","author":"Lynch Nancy A.","key":"e_1_2_1_63_1","unstructured":"Nancy A. Lynch . 1996. Distributed Algorithms . Morgan Kaufmann Publishers Inc .. Nancy A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann Publishers Inc.."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359651"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158134"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_2_1_67_1","unstructured":"Microsoft Coyote. 2022. Fearless coding for reliable asynchronous software. https:\/\/github.com\/microsoft\/coyote \t\t\t\t  Microsoft Coyote. 2022. Fearless coding for reliable asynchronous software. https:\/\/github.com\/microsoft\/coyote"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428298"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_3"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_22"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276530"},{"key":"e_1_2_1_73_1","unstructured":"P-GitHub. 2023. The P Programming Langugage. https:\/\/github.com\/p-org\/P \t\t\t\t  P-GitHub. 2023. The P Programming Langugage. https:\/\/github.com\/p-org\/P"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_6"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7814715"},{"key":"e_1_2_1_77_1","volume-title":"Psym: Efficient Symbolic Exploration of Distributed Systems (Extended Version). https:\/\/lmpick.github.io\/psym-extended.pdf","author":"Pick Lauren","year":"2023","unstructured":"Lauren Pick , Ankush Desai , and Aarti Gupta . 2023 . Psym: Efficient Symbolic Exploration of Distributed Systems (Extended Version). https:\/\/lmpick.github.io\/psym-extended.pdf Lauren Pick, Ankush Desai, and Aarti Gupta. 2023. Psym: Efficient Symbolic Exploration of Distributed Systems (Extended Version). https:\/\/lmpick.github.io\/psym-extended.pdf"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_7"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_18"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693017_25"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_38"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786830"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2018.8556946"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30793-5_14"},{"key":"e_1_2_1_86_1","unstructured":"TLA^+. 2021. Chang-Roberts algorithm for leader election in a ring. https:\/\/github.com\/tlaplus\/Examples\/tree\/616c4c2e00dd7084c623d1dcc83b140279652fb4\/specifications\/chang_roberts \t\t\t\t  TLA^+. 2021. Chang-Roberts algorithm for leader election in a ring. https:\/\/github.com\/tlaplus\/Examples\/tree\/616c4c2e00dd7084c623d1dcc83b140279652fb4\/specifications\/chang_roberts"},{"key":"e_1_2_1_87_1","unstructured":"TLA^+. 2023. TLA^+ Examples. https:\/\/github.com\/tlaplus\/Examples \t\t\t\t  TLA^+. 2023. TLA^+ Examples. https:\/\/github.com\/tlaplus\/Examples"},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050043"},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"volume-title":"DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols","author":"Yao Jianan","key":"e_1_2_1_91_1","unstructured":"Jianan Yao , Runzhou Tao , Ronghui Gu , Jason Nieh , Suman Jana , and Gabriel Ryan . 2021. DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols . In OSDI. USENIX Association , 405\u2013421. Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. 2021. DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In OSDI. USENIX Association, 405\u2013421."},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48153-2_6"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591247","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591247","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:47Z","timestamp":1750178867000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591247"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":92,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591247"],"URL":"https:\/\/doi.org\/10.1145\/3591247","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}