{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,23]],"date-time":"2024-09-23T04:31:14Z","timestamp":1727065874546},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"We present WasmRef-Isabelle, a monadic interpreter for WebAssembly written in Isabelle\/HOL and proven correct with respect to the WasmCert-Isabelle mechanisation of WebAssembly. WasmRef-Isabelle has been adopted and deployed as a fuzzing oracle in the continuous integration infrastructure of Wasmtime, a widely used WebAssembly implementation. Previous efforts to fuzz Wasmtime against WebAssembly's official OCaml reference interpreter were abandoned by Wasmtime's developers after the reference interpreter exhibited unacceptable performance characteristics, which its maintainers decided not to fix in order to preserve the interpreter's close definitional correspondence with the official specification. With WasmRef-Isabelle, we achieve the best of both worlds - an interpreter fast enough to be useable as a fuzzing oracle that also maintains a close correspondence with the specification through a mechanised proof of correctness.<\/jats:p>\n We verify the correctness of WasmRef-Isabelle through a two-step refinement proof in Isabelle\/HOL. We demonstrate that WasmRef-Isabelle significantly outperforms the official reference interpreter, has performance comparable to a Rust debug build of the industry WebAssembly interpreter Wasmi, and competes with unverified oracles on fuzzing throughput when deployed in Wasmtime's fuzzing infrastructure. We also present several new extensions to WasmCert-Isabelle which enhance WasmRef-Isabelle's utility as a fuzzing oracle: we add support for a number of upcoming WebAssembly features, and fully mechanise the numeric semantics of WebAssembly's integer operations.<\/jats:p>","DOI":"10.1145\/3591224","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"100-123","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"http:\/\/orcid.org\/0000-0002-0596-877X","authenticated-orcid":false,"given":"Conrad","family":"Watt","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}]},{"ORCID":"http:\/\/orcid.org\/0009-0000-2174-7902","authenticated-orcid":false,"given":"Maja","family":"Trela","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK \/ Jane Street, UK"}]},{"ORCID":"http:\/\/orcid.org\/0000-0003-3576-0504","authenticated-orcid":false,"given":"Peter","family":"Lammich","sequence":"additional","affiliation":[{"name":"University of Twente, Netherlands"}]},{"ORCID":"http:\/\/orcid.org\/0009-0006-6862-8330","authenticated-orcid":false,"given":"Florian","family":"M\u00e4rkl","sequence":"additional","affiliation":[{"name":"TU Munich, Germany"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"The B-Book: Assigning Programs to Meanings","author":"Abrial Jean-Raymond","unstructured":"Jean-Raymond Abrial . 1996. The B-Book: Assigning Programs to Meanings . Cambridge University Press . Jean-Raymond Abrial. 1996. The B-Book: Assigning Programs to Meanings. Cambridge University Press."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2920-7_9"},{"key":"e_1_2_1_3_1","unstructured":"Ralph-Johan Back and Joakim von Wright. 1998. Refinement Calculus \u2014 A Systematic Introduction. \t\t\t\t Ralph-Johan Back and Joakim von Wright. 1998. Refinement Calculus \u2014 A Systematic Introduction."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2372785"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535876"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676982"},{"key":"e_1_2_1_8_1","volume-title":"TPHOLs","author":"Bulwahn Lukas","year":"2008","unstructured":"Lukas Bulwahn , Alexander Krauss , Florian Haftmann , Levent Erk\u00f6k , and John Matthews . 2008. Imperative Functional Programming with Isabelle\/HOL . In TPHOLs 2008 , Otmane A\u00eft Mohamed, C\u00e9sar A. Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.) (LNCS , Vol. 5170). Springer, 134\u2013 149 . Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erk\u00f6k, and John Matthews. 2008. Imperative Functional Programming with Isabelle\/HOL. In TPHOLs 2008, Otmane A\u00eft Mohamed, C\u00e9sar A. Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.) (LNCS, Vol. 5170). Springer, 134\u2013149."},{"key":"e_1_2_1_9_1","unstructured":"Bytecode Alliance. 2022. Bytecode Alliance. https:\/\/bytecodealliance.org\/ \t\t\t\t Bytecode Alliance. 2022. Bytecode Alliance. https:\/\/bytecodealliance.org\/"},{"key":"e_1_2_1_10_1","unstructured":"Bytecode Alliance. 2022. wasmtime. https:\/\/github.com\/bytecodealliance\/wasmtime \t\t\t\t Bytecode Alliance. 2022. wasmtime. https:\/\/github.com\/bytecodealliance\/wasmtime"},{"key":"e_1_2_1_11_1","volume-title":"Mathematics of Program Construction: 13th International Conference, MPC 2019, Porto, Portugal, 2019, Proceedings. Springer-Verlag","author":"Chapman James","year":"2019","unstructured":"James Chapman , Roman Kireev , Chad Nester , and Philip Wadler . 2019 . System F in Agda, for Fun and Profit . In Mathematics of Program Construction: 13th International Conference, MPC 2019, Porto, Portugal, 2019, Proceedings. Springer-Verlag , Berlin, Heidelberg. 43 pages. James Chapman, Roman Kireev, Chad Nester, and Philip Wadler. 2019. System F in Agda, for Fun and Profit. In Mathematics of Program Construction: 13th International Conference, MPC 2019, Porto, Portugal, 2019, Proceedings. Springer-Verlag, Berlin, Heidelberg. 43 pages."},{"key":"e_1_2_1_12_1","unstructured":"ClusterFuzz. 2022. wasmtime:differential_spec: ASSERT: assertion failed. https:\/\/bugs.chromium.org\/p\/oss-fuzz\/issues\/detail?id=47918 \t\t\t\t ClusterFuzz. 2022. wasmtime:differential_spec: ASSERT: assertion failed. https:\/\/bugs.chromium.org\/p\/oss-fuzz\/issues\/detail?id=47918"},{"key":"e_1_2_1_13_1","volume-title":"CPP","volume":"162","author":"Cohen Cyril","year":"2013","unstructured":"Cyril Cohen , Maxime D\u00e9n\u00e8s , and Anders M\u00f6rtberg . 2013 . Refinements for Free! . In CPP 2013, Georges Gonthier and Michael Norrish (Eds.) (LNCS , Vol. 8307). Springer, 147\u2013 162 . Cyril Cohen, Maxime D\u00e9n\u00e8s, and Anders M\u00f6rtberg. 2013. Refinements for Free!. In CPP 2013, Georges Gonthier and Michael Norrish (Eds.) (LNCS, Vol. 8307). Springer, 147\u2013162."},{"key":"e_1_2_1_14_1","unstructured":"Alex Crichton. 2021. Timeouts in spec interpreter fuzzing.. https:\/\/github.com\/bytecodealliance\/wasmtime\/issues\/3186 \t\t\t\t Alex Crichton. 2021. Timeouts in spec interpreter fuzzing.. https:\/\/github.com\/bytecodealliance\/wasmtime\/issues\/3186"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_2_1_16_1","unstructured":"Chris Fallin. 2021. [interpreter] Fix quadratic behavior when stepping in deeply-nested scopes.. https:\/\/github.com\/WebAssembly\/spec\/pull\/1354 \t\t\t\t Chris Fallin. 2021. [interpreter] Fix quadratic behavior when stepping in deeply-nested scopes.. https:\/\/github.com\/WebAssembly\/spec\/pull\/1354"},{"key":"e_1_2_1_17_1","unstructured":"Shay Gal-On and Markus Levy. 2009. CoreMark. https:\/\/www.eembc.org\/techlit\/articles\/coremark-whitepaper.pdf \t\t\t\t Shay Gal-On and Markus Levy. 2009. CoreMark. https:\/\/www.eembc.org\/techlit\/articles\/coremark-whitepaper.pdf"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/202529.202541"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the 24th European Conference on Object-Oriented Programming (ECOOP\u201910)","author":"Guha Arjun","year":"2010","unstructured":"Arjun Guha , Claudiu Saftoiu , and Shriram Krishnamurthi . 2010 . The Essence of Javascript . In Proceedings of the 24th European Conference on Object-Oriented Programming (ECOOP\u201910) . Springer-Verlag, Berlin, Heidelberg. 126\u2013150. isbn:3642141064 Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. 2010. The Essence of Javascript. In Proceedings of the 24th European Conference on Object-Oriented Programming (ECOOP\u201910). Springer-Verlag, Berlin, Heidelberg. 126\u2013150. isbn:3642141064"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062363"},{"key":"e_1_2_1_21_1","unstructured":"Florian Haftmann and Lukas Bulwahn. 2021. Code generation from Isabelle\/HOL theories. https:\/\/isabelle.in.tum.de\/doc\/codegen.pdf \t\t\t\t Florian Haftmann and Lukas Bulwahn. 2021. Code generation from Isabelle\/HOL theories. https:\/\/isabelle.in.tum.de\/doc\/codegen.pdf"},{"key":"e_1_2_1_22_1","volume-title":"Turner","author":"He Ji","year":"1999","unstructured":"Ji He and Kenneth J . Turner . 1999 . Protocol-Inspired Hardware Testing. In IWTCS. Ji He and Kenneth J. Turner. 1999. Protocol-Inspired Hardware Testing. In IWTCS."},{"key":"e_1_2_1_23_1","volume-title":"International Conference on Interactive Theorem Proving. 269\u2013284","author":"Heule Marijn","year":"2017","unstructured":"Marijn Heule , Warren Hunt , Matt Kaufmann , and Nathan Wetzler . 2017 . Efficient, verified checking of propositional proofs . In International Conference on Interactive Theorem Proving. 269\u2013284 . Marijn Heule, Warren Hunt, Matt Kaufmann, and Nathan Wetzler. 2017. Efficient, verified checking of propositional proofs. In International Conference on Interactive Theorem Proving. 269\u2013284."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1459352.1459354"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00066"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"e_1_2_1_30_1","volume-title":"The C standard formalized in Coq. Ph. D. Dissertation","author":"Krebbers Robbert","unstructured":"Robbert Krebbers . 2015. The C standard formalized in Coq. Ph. D. Dissertation . Radboud University Nijmegen . Robbert Krebbers. 2015. The C standard formalized in Coq. Ph. D. Dissertation. Radboud University Nijmegen."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_1_32_1","volume-title":"ITP (LNCS","volume":"99","author":"Lammich Peter","year":"2013","unstructured":"Peter Lammich . 2013 . Automatic Data Refinement . In ITP (LNCS , Vol. 7998). Springer, 84\u2013 99 . Peter Lammich. 2013. Automatic Data Refinement. In ITP (LNCS, Vol. 7998). Springer, 84\u201399."},{"key":"e_1_2_1_33_1","volume-title":"ITP (LNCS","volume":"269","author":"Lammich Peter","year":"2015","unstructured":"Peter Lammich . 2015 . Refinement to Imperative\/HOL . In ITP (LNCS , Vol. 9236). Springer, 253\u2013 269 . Peter Lammich. 2015. Refinement to Imperative\/HOL. In ITP (LNCS, Vol. 9236). Springer, 253\u2013269."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09525-z"},{"key":"e_1_2_1_35_1","unstructured":"Peter Lammich and Rene Meis. 2012. A Separation Logic Framework for Imperative HOL. Archive of Formal Proofs November issn:2150-914x https:\/\/isa-afp.org\/entries\/Separation_Logic_Imperative_HOL.html \t\t\t\t Peter Lammich and Rene Meis. 2012. A Separation Logic Framework for Imperative HOL. Archive of Formal Proofs November issn:2150-914x https:\/\/isa-afp.org\/entries\/Separation_Logic_Imperative_HOL.html"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190245"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_38_1","unstructured":"LLVM Progect. 2022. LibFuzzer. https:\/\/llvm.org\/docs\/LibFuzzer.html \t\t\t\t LLVM Progect. 2022. LibFuzzer. https:\/\/llvm.org\/docs\/LibFuzzer.html"},{"key":"e_1_2_1_39_1","volume-title":"Fast Machine Words in Isabelle\/HOL","author":"Lochbihler Andreas","unstructured":"Andreas Lochbihler . 2018. Fast Machine Words in Isabelle\/HOL . In Interactive Theorem Proving, Jeremy Avigad and Assia Mahboubi (Eds.). Springer International Publishing , Cham . 388\u2013410. isbn:978-3-319-94821-8 Andreas Lochbihler. 2018. Fast Machine Words in Isabelle\/HOL. In Interactive Theorem Proving, Jeremy Avigad and Assia Mahboubi (Eds.). Springer International Publishing, Cham. 388\u2013410. isbn:978-3-319-94821-8"},{"key":"e_1_2_1_40_1","unstructured":"Michael Norrish. 1998. C formalised in HOL. \t\t\t\t Michael Norrish. 1998. C formalised in HOL."},{"key":"e_1_2_1_41_1","unstructured":"Parity Technologies. 2022. wasmi. https:\/\/github.com\/paritytech\/wasmi \t\t\t\t Parity Technologies. 2022. wasmi. https:\/\/github.com\/paritytech\/wasmi"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737991"},{"key":"e_1_2_1_43_1","volume-title":"Manually Managed Memory, and Proofs","author":"Pit-Claudel Cl\u00e9ment","unstructured":"Cl\u00e9ment Pit-Claudel , Peng Wang , Benjamin Delaware , Jason Gross , and Adam Chlipala . 2020. Extensible Extraction of Efficient Imperative Programs with Foreign Functions , Manually Managed Memory, and Proofs . In Automated Reasoning, Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.). Springer International Publishing , Cham . 119\u2013137. isbn:978-3-030-51054-1 Cl\u00e9ment Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, and Adam Chlipala. 2020. Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. In Automated Reasoning, Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.). Springer International Publishing, Cham. 119\u2013137. isbn:978-3-030-51054-1"},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Robert H. Pollack. 1996. How to Believe a Machine-Checked Proof 1. \t\t\t\t Robert H. Pollack. 1996. How to Believe a Machine-Checked Proof 1.","DOI":"10.7146\/brics.v4i18.18945"},{"key":"e_1_2_1_45_1","volume-title":"Proc of. Logic in Computer Science (LICS). IEEE, 55\u201374","author":"Reynolds John C.","year":"2002","unstructured":"John C. Reynolds . 2002 . Separation Logic: A Logic for Shared Mutable Data Structures . In Proc of. Logic in Computer Science (LICS). IEEE, 55\u201374 . John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc of. Logic in Computer Science (LICS). IEEE, 55\u201374."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815411"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_2_1_48_1","volume-title":"SpecTest: Specification-Based Compiler Testing. Fundamental Approaches to Software Engineering, 12649","author":"Schumi Richard","year":"2021","unstructured":"Richard Schumi and Jun Sun . 2021. SpecTest: Specification-Based Compiler Testing. Fundamental Approaches to Software Engineering, 12649 ( 2021 ). Richard Schumi and Jun Sun. 2021. SpecTest: Specification-Based Compiler Testing. Fundamental Approaches to Software Engineering, 12649 (2021)."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2011.5763028"},{"key":"e_1_2_1_50_1","unstructured":"TC39. 2018. SIMD.js. https:\/\/github.com\/tc39\/ecmascript_simd \t\t\t\t TC39. 2018. SIMD.js. https:\/\/github.com\/tc39\/ecmascript_simd"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563311"},{"key":"e_1_2_1_52_1","unstructured":"W3C. 2019. WebAssembly Core Specification. https:\/\/www.w3.org\/TR\/wasm-core-1\/ \t\t\t\t W3C. 2019. WebAssembly Core Specification. https:\/\/www.w3.org\/TR\/wasm-core-1\/"},{"key":"e_1_2_1_53_1","unstructured":"wasm3. 2021. was-coremark. https:\/\/github.com\/wasm3\/wasm-coremark \t\t\t\t wasm3. 2021. was-coremark. https:\/\/github.com\/wasm3\/wasm-coremark"},{"key":"e_1_2_1_54_1","unstructured":"WasmCert. 2023. WasmRef-Isabelle. https:\/\/github.com\/WasmCert\/WasmCert-Isabelle \t\t\t\t WasmCert. 2023. WasmRef-Isabelle. https:\/\/github.com\/WasmCert\/WasmCert-Isabelle"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167082"},{"key":"e_1_2_1_56_1","volume-title":"Two Mechanisations of WebAssembly 1.0","author":"Watt Conrad","unstructured":"Conrad Watt , Xiaojia Rao , Jean Pichon-Pharabod , Martin Bodin , and Philippa Gardner . 2021. Two Mechanisations of WebAssembly 1.0 . In Formal Methods, Marieke Huisman, Corina P\u0103s\u0103reanu, and Naijun Zhan (Eds.). Springer International Publishing , Cham . 61\u201379. isbn:978-3-030-90870-6 Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, and Philippa Gardner. 2021. Two Mechanisations of WebAssembly 1.0. In Formal Methods, Marieke Huisman, Corina P\u0103s\u0103reanu, and Naijun Zhan (Eds.). Springer International Publishing, Cham. 61\u201379. isbn:978-3-030-90870-6"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7815663"},{"key":"e_1_2_1_58_1","unstructured":"WebAssembly Community Group. 2019. nontrapping-float-to-int-conversions. https:\/\/github.com\/WebAssembly\/nontrapping-float-to-int-conversions \t\t\t\t WebAssembly Community Group. 2019. nontrapping-float-to-int-conversions. https:\/\/github.com\/WebAssembly\/nontrapping-float-to-int-conversions"},{"key":"e_1_2_1_59_1","unstructured":"WebAssembly Community Group. 2020. multi-value. https:\/\/github.com\/WebAssembly\/multi-value \t\t\t\t WebAssembly Community Group. 2020. multi-value. https:\/\/github.com\/WebAssembly\/multi-value"},{"key":"e_1_2_1_60_1","unstructured":"WebAssembly Community Group. 2021. bulk memory. https:\/\/github.com\/WebAssembly\/bulk-memory-operations \t\t\t\t WebAssembly Community Group. 2021. bulk memory. https:\/\/github.com\/WebAssembly\/bulk-memory-operations"},{"key":"e_1_2_1_61_1","unstructured":"WebAssembly Community Group. 2021. reference types. https:\/\/github.com\/WebAssembly\/reference-types \t\t\t\t WebAssembly Community Group. 2021. reference types. https:\/\/github.com\/WebAssembly\/reference-types"},{"key":"e_1_2_1_62_1","unstructured":"WebAssembly Community Group. 2021. simd. https:\/\/github.com\/WebAssembly\/simd \t\t\t\t WebAssembly Community Group. 2021. simd. https:\/\/github.com\/WebAssembly\/simd"},{"key":"e_1_2_1_63_1","unstructured":"WebAssembly Community Group. 2021. threads. https:\/\/github.com\/WebAssembly\/threads \t\t\t\t WebAssembly Community Group. 2021. threads. https:\/\/github.com\/WebAssembly\/threads"},{"key":"e_1_2_1_64_1","unstructured":"WebAssembly Community Group. 2022. gc. https:\/\/github.com\/WebAssembly\/gc \t\t\t\t WebAssembly Community Group. 2022. gc. https:\/\/github.com\/WebAssembly\/gc"},{"key":"e_1_2_1_65_1","unstructured":"WebAssembly Community Group. 2022. WebAssembly\/spec\/interpreter. https:\/\/github.com\/WebAssembly\/spec\/tree\/main\/interpreter \t\t\t\t WebAssembly Community Group. 2022. WebAssembly\/spec\/interpreter. https:\/\/github.com\/WebAssembly\/spec\/tree\/main\/interpreter"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_34"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591224","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:27:26Z","timestamp":1686083246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591224"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":67,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591224"],"URL":"https:\/\/doi.org\/10.1145\/3591224","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"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"}}]}}
