{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:37Z","timestamp":1784837797955,"version":"3.55.0"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"DOI":"10.13039\/100018693","name":"Horizon Europe","doi-asserted-by":"crossref","award":["101070375"],"award-info":[{"award-number":["101070375"]}],"id":[{"id":"10.13039\/100018693","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>\n                    Bit-blasting SMT solvers enable efficient automatic reasoning about bitvectors, which are fundamental for the verification of compiler backends, cryptographic algorithms, hardware designs and other soft- or hardware tasks. Despite the clear demand for efficient bitvector reasoning infrastructure and the impressive advancements in state-of-the-art bit-blasting SMT solvers such as Bitwuzla, effective bitvector reasoning within interactive theorem provers (ITPs) remains a challenge, hindering their use for mechanized proofs. Incomplete bitvector libraries, unavailable or only partially integrated decision procedures, complex and hard-to-bitblast operations, and limited integration with the host language prevent the wide adoption of bitvector reasoning in proving contexts. We introduce\n                    <jats:monospace>bv_decide<\/jats:monospace>\n                    :\n                    <jats:italic toggle=\"yes\">the first end-to-end verified bitblaster designed for interactive bitvector reasoning in a dependently-typed ITP<\/jats:italic>\n                    . Our verified bitblaster is scalable, comes with a complete end-to-end proof (trusting only the Lean compiler and kernel), and is available as a proof tactic that allows interactive reasoning right from within a programming language, in our case Lean. We use Lean\u2019s Functional But In-Place (FBIP) paradigm to efficiently encode our core data structures (e.g., AIGs), demonstrating that fast execution of an SMT solver need not come at the expense of rigorous formalization. We enable dependable interactive verification of user-written-code by basing Lean\u2019s C-Style standard dataypes UInt\/SInt on our bitvector type, adding a lowering from enums and structs to bitvectors to enable transparent bit-blasting support for composed types, and by offering an interactive tactic that either solves a goal or provides a counter-example. Moreover, we present the design of Lean\u2019s canonical bitvector library, which supports all operations (with reasoning principles) for the SMT-LIB 2.7 standard (including overflow modeling), is fast-to-execute, and offers a comprehensive API and automation for bit-width-independent reasoning. We thoroughly evaluate our bit-blaster on a comprehensive set of benchmarks, including the full SMT-LIB dataset, where\n                    <jats:monospace>bv_decide<\/jats:monospace>\n                    solves more theorems than the state-of-the-art in verified bit-blasting, CoqQFBV. We also verify over 7000 SMT statements extracted from LLVM, providing the largest mechanized verification of LLVM rewrites to date, to our knowledge. By making bit-blasting bitvector reasoning a polished, well-supported, and interactive feature of modern ITPs, we enable effective, dependable white-box reasoning for bitvector-level verification.\n                  <\/jats:p>","DOI":"10.1145\/3763167","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"3259-3285","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Interactive Bitvector Reasoning using Verified Bit-Blasting"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-8294-2710","authenticated-orcid":false,"given":"Henrik","family":"B\u00f6ving","sequence":"first","affiliation":[{"name":"Lean FRO, Munich, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-6410-3681","authenticated-orcid":false,"given":"Siddharth","family":"Bhat","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8826-9607","authenticated-orcid":false,"given":"Luisa","family":"Cicolini","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-9831-6968","authenticated-orcid":false,"given":"Alex","family":"Keizer","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-1880-0602","authenticated-orcid":false,"given":"L\u00e9on","family":"Frenot","sequence":"additional","affiliation":[{"name":"ENS Lyon, Lyon, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1414-7073","authenticated-orcid":false,"given":"Abdalrhman","family":"Mohamed","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4719-2922","authenticated-orcid":false,"given":"L\u00e9o","family":"Stefanesco","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3379-5631","authenticated-orcid":false,"given":"Harun","family":"Khan","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4047-6196","authenticated-orcid":false,"given":"Joshua","family":"Clune","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3874-6003","authenticated-orcid":false,"given":"Tobias","family":"Grosser","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"issue":"1","key":"e_1_3_1_5_2","first-page":"23","article-title":"Proofs in satisfiability modulo theories","volume":"55","author":"Barrett Clark","year":"2015","unstructured":"Clark Barrett, Leonardo De Moura, and Pascal Fontaine. 2015. Proofs in satisfiability modulo theories. All about proofs, Proofs for all 55, 1 (2015), 23\u201344.","journal-title":"All about proofs, Proofs for all"},{"key":"e_1_3_1_6_2","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2024. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org."},{"issue":"14","key":"e_1_3_1_7_2","article-title":"The smt-lib standard: Version 2.0","volume":"13","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett, Aaron Stump, Cesare Tinelli, et al. 2010. The smt-lib standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK), Vol. 13. 14.","journal-title":"Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK)"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277186"},{"key":"e_1_3_1_9_2","article-title":"Finite Machine Word Library","author":"Beeren Joel","year":"2016","unstructured":"Joel Beeren, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski, Japheth Lim, Corey Lewis, Daniel Matichuk, and Thomas Sewell. 2016. Finite Machine Word Library. Archive of Formal Proofs (2016).","journal-title":"Archive of Formal Proofs"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2407.03685"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_7"},{"key":"e_1_3_1_12_2","first-page":"8","volume-title":"Proc. of SAT Competition 2024 \u2013 Solver, Benchmark and Proof Checker Descriptions (Department of Computer Science Report Series B, Vol. B-2024-1)","author":"Biere Armin","year":"2024","unstructured":"Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. 2024. CaDiCaL, Gimsatul, IsaSAT and Kissat Entering the SAT Competition 2024. In Proc. of SAT Competition 2024 \u2013 Solver, Benchmark and Proof Checker Descriptions (Department of Computer Science Report Series B, Vol. B-2024-1), Marijn Heule, Markus Iser, Matti J\u00e4rvisalo, and Martin Suda (Eds.). University of Helsinki, 8\u201310."},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24364-6_2"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"e_1_3_1_15_2","unstructured":"Arthur Blot Pierre-Evariste Dagand and Julia Lawall. [n. d.]. Bit Sequences and Bit Sets Library. https:\/\/github.com\/pedagand\/ssrbit"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_15"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","unstructured":"Sylvie Boldo Jacques-Henri Jourdan Xavier Leroy and Guillaume Melquiond. 2013. A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. In 2013 IEEE 21st Symposium on Computer Arithmetic. 107\u2013115. https:\/\/doi.org\/10.1109\/ARITH.2013.30 10.1109\/ARITH.2013.30","DOI":"10.1109\/ARITH.2013.30"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2011.40"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","unstructured":"Thomas Bourgeat Cl\u00e9ment Pit-Claudel and Adam Chlipala. 2020. The essence of Bluespec: a core language for rule-based hardware design. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. 243\u2013257. https:\/\/doi.org\/10.1145\/3385412.3385965 10.1145\/3385412.3385965","DOI":"10.1145\/3385412.3385965"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","unstructured":"Henrik B\u00f6ving Siddharth Bhat Luisa Cicolini Alex Keizer L\u00e9on Frenot Abdalrhman Mohamed L\u00e9o Stefanesco Harun Khan Joshua Clune Clark Barrett and Tobias Grosser. 2025. Interactive Bit Vector Reasoning using Verified Bitblasting. https:\/\/doi.org\/10.5281\/zenodo.15762083 10.5281\/zenodo.15762083","DOI":"10.5281\/zenodo.15762083"},{"key":"e_1_3_1_22_2","unstructured":"Robert Brummayer and Armin Biere. 2006. Local Two-Level And-Inverter Graph Minimization without Blowup. https:\/\/api.semanticscholar.org\/CorpusID:14512831"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","unstructured":"Rosario Cammarota. 2022. Intel HERACLES: Homomorphic encryption revolutionary accelerator with correctness for learning-oriented end-to-end solutions. In Proceedings of the 2022 on Cloud Computing Security Workshop. 3\u20133. https:\/\/doi.org\/10.1145\/3560810.3565290 10.1145\/3560810.3565290","DOI":"10.1145\/3560810.3565290"},{"key":"e_1_3_1_25_2","unstructured":"Ted Chajed Haogang Chen Adam Chlipala Joonwon Choi Andres Erbsen Jason Gross Samuel Gruetter Frans Kaashoek Alex Konradi Gregory Malecha Duckki Oe Murali Vijayaraghavan Nickolai Zeldovich and Daniel Ziegler. [n. d.]. Bedrock Bitvectors Library. https:\/\/github.com\/mit-plv\/bbv"},{"key":"e_1_3_1_26_2","unstructured":"Microsoft Corporation. [n. d.]. Tactics | Online Z3 Guide. https:\/\/microsoft.github.io\/z3guide\/docs\/strategies\/tactics\/. Accessed: 2024-11-07."},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_14"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.114.8"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_1_30_2","unstructured":"Jean Duprat. [n. d.]. Coq.Bool.BVector Library. https:\/\/coq.inria.fr\/library\/Coq.Bool.Bvector.html"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_1_33_2","volume-title":"Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT. Ph. D. Dissertation","author":"Franz\u00e9n Anders","year":"2010","unstructured":"Anders Franz\u00e9n. 2010. Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT. Ph. D. Dissertation. University of Trento, Italy. http:\/\/eprints-phd.biblio.unitn.it\/345\/"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/1979"},{"issue":"2","key":"e_1_3_1_36_2","article-title":"Gnu mp","volume":"2","author":"Granlund Torbj\u00f6rn","year":"1996","unstructured":"Torbj\u00f6rn Granlund. 1996. Gnu mp. The GNU Multiple Precision Arithmetic Library 2, 2 (1996).","journal-title":"The GNU Multiple Precision Arithmetic Library"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_45"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031814"},{"key":"e_1_3_1_39_2","unstructured":"Joe Hurd. 2003. First-order proof tactics in higher-order logic theorem provers. Design and Application of Strategies\/Tactics in Higher Order Logics number NASA\/CP-2003-212448 in NASA Technical Reports (2003) 56\u201368."},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_53"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/CMPASS.1996.507872"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66263-3_29"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_28"},{"key":"e_1_3_1_45_2","unstructured":"Lean FRO. 2025. Lean-MLIR GitHub. https:\/\/github.com\/opencompl\/lean-mlir"},{"key":"e_1_3_1_46_2","unstructured":"Lean FRO. 2025. Lean4 GitHub. https:\/\/github.com\/leanprover\/lean4"},{"key":"e_1_3_1_47_2","unstructured":"Xavier Leroy Sandrine Blazy Daniel K\u00e4stner Bernhard Schommer Markus Pister and Christian Ferdinand. 2016. CompCert-a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems 8th European Congress."},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","unstructured":"Nuno P Lopes Juneyoung Lee Chung-Kil Hur Zhengyang Liu and John Regehr. 2021. Alive2: bounded translation validation for LLVM. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 65\u201379. https:\/\/doi.org\/10.1145\/3453483.3454030 10.1145\/3453483.3454030","DOI":"10.1145\/3453483.3454030"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","unstructured":"Robert B Miller. 1968. Response time in man-computer conversational transactions. In Proceedings of the December 9-11 1968 fall joint computer conference part I. 267\u2013277. https:\/\/doi.org\/10.1145\/1476589.1476628 10.1145\/1476589.1476628","DOI":"10.1145\/1476589.1476628"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"e_1_3_1_52_2","unstructured":"SMT-COMP Organizers. 2024. SMT-COMP 2024 Results. Online. https:\/\/smt-comp.github.io\/2024\/results.html Accessed: 2025-03-25."},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","unstructured":"Yan Peng and Mark Greenstreet. 2015. Extending ACL2 with SMT solvers. arXiv preprint arXiv:1509.06082 (2015). https:\/\/doi.org\/10.4204\/EPTCS.192.6 10.4204\/EPTCS.192.6","DOI":"10.4204\/EPTCS.192.6"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","unstructured":"Florian Pollitt Mathias Fleury and Armin Biere. 2023. Faster LRAT Checking Than Solving with CaDiCaL. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik. https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2023.21 10.4230\/LIPIcs.SAT.2023.21","DOI":"10.4230\/LIPIcs.SAT.2023.21"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"e_1_3_1_56_2","unstructured":"David M Russinoff. 2017. Polynomial terms and sparse horner normal form."},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3408997"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_7"},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","unstructured":"Tobias Stelzer Felix Oberhansl Jonas Schupp and Patrick Karl. 2023. Enabling Lattice-Based Post-Quantum Cryptography on the OpenTitan Platform. In Proceedings of the 2023 Workshop on Attacks and Solutions in Hardware Security. 51\u201360. https:\/\/doi.org\/10.1145\/3605769.3623993 10.1145\/3605769.3623993","DOI":"10.1145\/3605769.3623993"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0163-3"},{"key":"e_1_3_1_61_2","unstructured":"Nikhil Swamy Guido Martinez and Aseem Rastogi. 2023. Proof-Oriented Programming in F*."},{"key":"e_1_3_1_62_2","doi-asserted-by":"publisher","unstructured":"Sol Swords and Jared Davis. 2011. Bit-blasting ACL2 theorems. arXiv preprint arXiv:1110.4676 (2011). https:\/\/doi.org\/10.4204\/EPTCS.70.7 10.4204\/EPTCS.70.7","DOI":"10.4204\/EPTCS.70.7"},{"key":"e_1_3_1_63_2","doi-asserted-by":"publisher","unstructured":"Grigori S Tseitin. 1983. On the complexity of derivation in propositional calculus. Automation of reasoning: 2: Classical papers on computational logic 1967-1970 (1983) 466\u2013483. https:\/\/doi.org\/10.1007\/978-3-642-81955-1_28 10.1007\/978-3-642-81955-1_28","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"e_1_3_1_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/3412932.3412935"},{"key":"e_1_3_1_65_2","volume-title":"Hacker\u2019s delight","author":"Warren Henry S","year":"2013","unstructured":"Henry S Warren. 2013. Hacker\u2019s delight. Pearson Education."},{"key":"e_1_3_1_66_2","volume-title":"DeepSpec: Modular Certified Programming with Deep Specifications","author":"Weng Shu-Chun","year":"2016","unstructured":"Shu-Chun Weng. 2016. DeepSpec: Modular Certified Programming with Deep Specifications. Yale University."},{"key":"e_1_3_1_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_7"},{"key":"e_1_3_1_68_2","doi-asserted-by":"publisher","unstructured":"Jianzhou Zhao Santosh Nagarakatte Milo MK Martin and Steve Zdancewic. 2012. Formalizing the LLVM intermediate representation for verified program transformations. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 427\u2013440. https:\/\/doi.org\/10.1145\/2103656.2103709 10.1145\/2103656.2103709","DOI":"10.1145\/2103656.2103709"},{"key":"e_1_3_1_69_2","doi-asserted-by":"publisher","unstructured":"Jean-Karim Zinzindohou\u00e9 Karthikeyan Bhargavan Jonathan Protzenko and Benjamin Beurdouche. 2017. HACL*: A verified modern cryptographic library. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. 1789\u20131806. https:\/\/doi.org\/10.1145\/3133956.3134043 10.1145\/3133956.3134043","DOI":"10.1145\/3133956.3134043"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763167","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:17:32Z","timestamp":1784197052000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763167"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":68,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763167"],"URL":"https:\/\/doi.org\/10.1145\/3763167","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}