{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:22:57Z","timestamp":1787592177100,"version":"build-2736575974"},"reference-count":75,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>\n                    Program verifiers such as Dafny automate proofs by outsourcing them to an SMT solver. This automation is not perfect, however, and the solver often requires hints in the form of\n                    <jats:italic toggle=\"yes\">assertions,<\/jats:italic>\n                    creating a burden for the proof engineer. In this paper, we propose Laurel, a tool that alleviates this burden by automatically generating assertions using large language models (LLMs).\n                  <\/jats:p>\n                  <jats:p>\n                    To improve the success rate of LLMs in this task, we design two domain-specific prompting techniques. First, we help the LLM determine the location of the missing assertion by analyzing the verifier\u2019s error message and inserting an\n                    <jats:italic toggle=\"yes\">assertion placeholder<\/jats:italic>\n                    at that location. Second, we provide the LLM with example assertions from the same codebase, which we select based on a new\n                    <jats:italic toggle=\"yes\">proof similarity<\/jats:italic>\n                    metric. We evaluate our techniques on our new benchmark\n                    <jats:sc>DafnyGym<\/jats:sc>\n                    , a dataset of complex lemmas we extracted from three real-world Dafny codebases. Our evaluation shows that\n                    <jats:sc>Laurel<\/jats:sc>\n                    is able to generate over\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mn>56.6<\/mml:mn>\n                          <mml:mtext>%<\/mml:mtext>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    of the required assertions given only a few attempts, making LLMs an affordable tool for unblocking program verifiers without human intervention.\n                  <\/jats:p>","DOI":"10.1145\/3720499","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1519-1545","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Laurel: Unblocking Automated Verification with Large Language Models"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-4967-6820","authenticated-orcid":false,"given":"Eric","family":"Mugnier","sequence":"first","affiliation":[{"name":"UC San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-9013-2228","authenticated-orcid":false,"given":"Emmanuel Anaya","family":"Gonzalez","sequence":"additional","affiliation":[{"name":"UC San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5571-173X","authenticated-orcid":false,"given":"Nadia","family":"Polikarpova","sequence":"additional","affiliation":[{"name":"UC San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1802-9421","authenticated-orcid":false,"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[{"name":"UC San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-0980-2538","authenticated-orcid":false,"given":"Zhou","family":"Yuanyuan","sequence":"additional","affiliation":[{"name":"UC San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"2023. Verification Optimization. https:\/\/dafny.org\/latest\/VerificationOptimization\/VerificationOptimization"},{"key":"e_1_3_1_3_1","unstructured":"2024. AWS Encryption SDK for Dafny. https:\/\/github.com\/aws\/aws-encryption-sdk-dafny."},{"key":"e_1_3_1_4_1","unstructured":"2024. Cedar. https:\/\/www.cedarpolicy.com\/."},{"key":"e_1_3_1_5_1","unstructured":"2024. Dafny-libraries. https:\/\/github.com\/dafny-lang\/libraries."},{"key":"e_1_3_1_6_1","unstructured":"2024. GPT-4o. https:\/\/platform.openai.com\/docs\/models\/gpt-4o."},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290353"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_3_1_10_1","unstructured":"Jacob Austin Augustus Odena Maxwell I. Nye Maarten Bosma Henryk Michalewski David Dohan Ellen Jiang Carrie J. Cai Michael Terry Quoc V. Le and Charles Sutton. 2021. Program Synthesis with Large Language Models. CoRR abs\/2108.07732 (2021). arXiv:2108.07732 https:\/\/arxiv.org\/abs\/2108.07732"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"Shraddha Barke Christian Poelitz Carina Negreanu Benjamin Zorn Jos\u00e9 Cambronero Andrew Gordon Vu Le Elnaz Nouri Nadia Polikarpova Advait Sarkar Brian Slininger Neil Toronto and Jack Williams. 2024. Solving Data-centric Tasks using Large Language Models. In Findings of the ACL Kevin Duh Helena Gomez and Steven Bethard (Eds.). doi:10.18653\/v1\/2024.findings-naacl.41","DOI":"10.18653\/v1\/2024.findings-naacl.41"},{"key":"e_1_3_1_12_1","unstructured":"David Brandfonbrener Simon Henniger Sibi Raja Tarun Prasad Chloe Loughridge Federico Cassano Sabrina Ruixin Hu Jianang Yang William E. Byrd Robert Zinkov and Nada Amin. 2024. VerMCTS: Synthesizing Multi-Step Programs using a Verifier a Large Language Model and Tree Search. arXiv:2402.08147 [cs.SE] https:\/\/arxiv.org\/abs\/2402.08147"},{"key":"e_1_3_1_13_1","unstructured":"Tom B. Brown Benjamin Mann Nick Ryder Melanie Subbiah Jared Kaplan Prafulla Dhariwal Arvind Neelakantan Pranav Shyam Girish Sastry Amanda Askell Sandhini Agarwal Ariel Herbert-Voss Gretchen Krueger Tom Henighan Rewon Child Aditya Ramesh Daniel M. Ziegler Jeffrey Wu Clemens Winter Christopher Hesse Mark Chen Eric Sigler Mateusz Litwin Scott Gray Benjamin Chess Jack Clark Christopher Berner Sam McCandlish Alec Radford Ilya Sutskever and Dario Amodei. 2020. Language models are few-shot learners (NIPS 20). https:\/\/dl.acm.org\/doi\/abs\/10.5555\/3495724.3495883"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Franck Cassez Joanne Fuller Milad K. Ghale David J. Pearce and Horacio M. A. Quiles. 2023. Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny. In Formal Methods Marsha Chechik Joost-Pieter Katoen and Martin Leucker (Eds.). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_32 10.1007\/978-3-031-27481-7_32","DOI":"10.1007\/978-3-031-27481-7_32"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE55347.2025.00002"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2023.findings-emnlp.614"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-015-1573-7"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","unstructured":"Mark Chen Jerry Tworek Heewoo Jun Qiming Yuan Henrique Ponde de Oliveira Pinto Jared Kaplan Harri Edwards Yuri Burda Nicholas Joseph Greg Brockman Alex Ray Raul Puri Gretchen Krueger Michael Petrov Heidy Khlaaf Girish Sastry Pamela Mishkin Brooke Chan Scott Gray Nick Ryder Mikhail Pavlov Alethea Power Lukasz Kaiser Mohammad Bavarian Clemens Winter Philippe Tillet Felipe Petroski Such Dave Cummings Matthias Plappert Fotios Chantzis Elizabeth Barnes Ariel Herbert-Voss William Hebgen Guss Alex Nichol Alex Paino Nikolas Tezak Jie Tang Igor Babuschkin Suchir Balaji Shantanu Jain William Saunders Christopher Hesse Andrew N. Carr Jan Leike Josh Achiam Vedant Misra Evan Morikawa Alec Radford Matthew Knight Miles Brundage Mira Murati Katie Mayer Peter Welinder Bob McGrew Dario Amodei Sam McCandlish Ilya Sutskever and Wojciech Zaremba. 2021. Evaluating Large Language Models Trained on Code. doi:10.48550\/arXiv.2107.03374 arXiv:2107.03374 [cs.LG]","DOI":"10.48550\/arXiv.2107.03374"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","unstructured":"Muslim Chochlov Gul Aftab Ahmed James Vincent Patten Guoxian Lu Wei Hou David Gregg and Jim Buckley. 2022. Using a Nearest-Neighbour BERT-Based Approach for Scalable Clone Detection. In 2022 IEEE International Conference on Software Maintenance and Evolution (ICSME). 582\u2013591. doi:10.1109\/ICSME55016.2022.00080","DOI":"10.1109\/ICSME55016.2022.00080"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj S. Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS. doi:10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Xavier Denis Jacques-Henri Jourdan and Claude March\u00e9. 2022. Creusot: A Foundry for the Deductive Verification of Rust Programs. In Formal Methods and Software Engineering Adrian Riesco and Min Zhang (Eds.). 90\u2013105. doi:10.1007\/978-3-031-17244-1_6","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSEC.2022.3153035"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","unstructured":"Jean-Christophe Filli\u00e2tre and Andrei Paskevich. 2013. Why3 \u2014 Where Programs Meet Provers. In Programming Languages and Systems Matthias Felleisen and Philippa Gardner (Eds.). doi:10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616243"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","unstructured":"R.W. Floyd. 1967. Assigning meanings to programs. In Mathematical Aspects of Computer Science. https:\/\/doi.org\/10.1007\/978-94-011-1793-7_4 10.1007\/978-94-011-1793-7_4","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"e_1_3_1_26_1","first-page":"165","volume-title":"11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14)","author":"Hawblitzel Chris","year":"2014","unstructured":"Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad Apps: End-to-End Security via Automated Full-System Verification. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14). USENIX Association, Broomfield, CO, 165\u2013181. https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/hawblitzel"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","unstructured":"Matthias Heizmann Jochen Hoenicke and Andreas Podelski. 2013. Software Model Checking for People Who Love Automata. In CAV Natasha Sharygina and Helmut Veith (Eds.). doi:10.1007\/978-3-642-39799-8_2","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","unstructured":"Lingxiao Jiang Ghassan Misherghi Zhendong Su and Stephane Glondu. 2007. DECKARD: Scalable and Accurate Tree-Based Detection of Code Clones. In 29th International Conference on Software Engineering (ICSE\u201907). 96\u2013105. doi:10.1109\/ICSE.2007.30","DOI":"10.1109\/ICSE.2007.30"},{"key":"e_1_3_1_29_1","unstructured":"Adharsh Kamath Aditya Senthilnathan Saikat Chakraborty Pantazis Deligiannis Shuvendu K. Lahiri Akash Lal Aseem Rastogi Subhajit Roy and Rahul Sharma. 2023. Finding Inductive Loop Invariants using Large Language Models. arXiv:2311.07948 [cs.PL] https:\/\/arxiv.org\/abs\/2311.07948"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2020.emnlp-main.550"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","unstructured":"Anirudh Khatry Joyce Cahoon Jordan Henkel Shaleen Deep Venkatesh Emani Avrilia Floratou Sumit Gulwani Vu Le Mohammad Raza Sherry Shi Mukul Singh and Ashish Tiwari. 2023. From Words to Code: Harnessing Data for Program Synthesis from Natural Language. arXiv:2305.01598 https:\/\/doi.org\/10.48550\/arXiv.2305.01598 10.48550\/arXiv.2305.01598","DOI":"10.48550\/arXiv.2305.01598"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Naoki Kobayashi Taro Sekiyama Issei Sato and Hiroshi Unno. 2021. Toward Neural-Network-Guided Program Synthesis and Verification. In Static Analysis Cezara Dr\u0103goi Suvam Mukherjee and Kedar Namjoshi (Eds.). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_12 10.1007\/978-3-030-88806-0_12","DOI":"10.1007\/978-3-030-88806-0_12"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_3_1_35_1","volume-title":"This is Boogie 2. Technical Report","author":"Leino K. Rustan M.","year":"2008","unstructured":"K. Rustan M. Leino. 2008. This is Boogie 2. Technical Report. Microsoft Research. https:\/\/www.microsoft.com\/enus\/research\/publication\/this-is-boogie-2\/"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","unstructured":"K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming Artificial Intelligence and Reasoning Edmund M. Clarke and Andrei Voronkov (Eds.). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20 10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_1_37_1","unstructured":"K. Rustan M. Leino Todd Millstein and James B. Saxe. 2005. Generating error traces from verification-condition counterexamples. Science of Computer Programming (2005). https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0167642304001510"},{"key":"e_1_3_1_38_1","unstructured":"Zhaoyu Li Jialiang Sun Logan Murphy Qidong Su Zenan Li Xian Zhang Kaiyu Yang and Xujie Si. 2024. A Survey on Deep Learning for Theorem Proving. arXiv:2404.09939 [cs.AI] https:\/\/arxiv.org\/abs\/2404.09939"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2022.deelio-1.10"},{"key":"e_1_3_1_40_1","unstructured":"Chloe Loughridge Qinyi Sun Seth Ahrenbach Federico Cassano Chuyue Sun Ying Sheng Anish Mudide Md Rakib Hossain Misu Nada Amin and Max Tegmark. 2024. DafnyBench: A Benchmark for Formal Software Verification. arXiv:2406.08467 [cs.SE] https:\/\/arxiv.org\/abs\/2406.08467"},{"key":"e_1_3_1_41_1","doi-asserted-by":"crossref","unstructured":"Yao Lu Max Bartolo Alastair Moore Sebastian Riedel and Pontus Stenetorp. 2022. Fantastically Ordered Prompts and Where to Find Them: Overcoming Few-Shot Prompt Order Sensitivity. In Proceedings of the 60th Annual Meeting of the ACL Smaranda Muresan Preslav Nakov and Aline Villavicencio (Eds.). https:\/\/aclanthology.org\/2022.acl-long.556","DOI":"10.18653\/v1\/2022.acl-long.556"},{"key":"e_1_3_1_42_1","unstructured":"Maciej Miku\u0142a Szymon Antoniak Szymon Tworkowski Bartosz Piotrowski Albert Jiang Jin Peng Zhou Christian Szegedy \u0141ukasz Kuci\u0144ski Piotr Mi\u0142o\u015b and Yuhuai Wu. 2023. Magnushammer: A Transformer-Based Approach to Premise Selection. In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS\u201923. https:\/\/openreview.net\/forum?id=WgaVCqZeIU"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3643763"},{"key":"e_1_3_1_44_1","unstructured":"Eric Mugnier Emmanuel Anaya Gonzalez Ranjit Jhala Nadia Polikarpova and Yuanyuan Zhou. 2024. Laurel: Unblocking Automated Verification with Large Language Models. arXiv:2405.16792 [cs.LO] https:\/\/arxiv.org\/abs\/2405.16792"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","unstructured":"Eric Mugnier Emmanuel Anaya Gonzalez Ranjit Jhala Nadia Polikarpova and Yuanyuan Zhou. 2025a. Artifact for OOPSLA 2025: \u2033Laurel: Unblocking Automated Verification with Large Language Models\u2033. doi:10.5281\/zenodo.14676571","DOI":"10.5281\/zenodo.14676571"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","unstructured":"Eric Mugnier Emmanuel Anaya Gonzalez Ranjit Jhala Nadia Polikarpova and Yuanyuan Zhou. 2025b. DafnyGym. https:\/\/doi.org\/10.5281\/zenodo.14676571 10.5281\/zenodo.14676571","DOI":"10.5281\/zenodo.14676571"},{"key":"e_1_3_1_47_1","unstructured":"Arvind Neelakantan Tao Xu Raul Puri Alec Radford Jesse Michael Han Jerry Tworek Qiming Yuan Nikolas Tezak Jong Wook Kim Chris Hallacy Johannes Heidecke Pranav Shyam Boris Power Tyna Eloundou Nekoul Girish Sastry Gretchen Krueger David Schnurr Felipe Petroski Such Kenny Hsu Madeleine Thompson Tabarak Khan Toki Sherbakov Joanne Jang Peter Welinder and Lilian Weng. 2022. Text and Code Embeddings by Contrastive Pre-Training. arXiv:2201.10005 [cs.CL] https:\/\/arxiv.org\/abs\/2201.10005"},{"key":"e_1_3_1_48_1","unstructured":"Kexin Pei David Bieber Kensen Shi Charles Sutton and Pengcheng Yin. [n. d.]. Can Large Language Models Reason about Program Invariants?. In ICML 2023 Andreas Krause Emma Brunskill Kyunghyun Cho Barbara Engelhardt Sivan Sabato and Jonathan Scarlett (Eds.). https:\/\/proceedings.mlr.press\/v202\/pei23a.html"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","unstructured":"Lutz Prechelt and Michael Phlippsen. 2000. JPlag: Finding plagiarisms among a set of programs. doi:10.5445\/IR\/542000","DOI":"10.5445\/IR\/542000"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","unstructured":"Jonathan Protzenko Bryan Parno Aymeric Fromherz Chris Hawblitzel Marina Polubelova Karthikeyan Bhargavan Benjamin Beurdouche Joonwon Choi Antoine Delignat-Lavaud C\u00e9dric Fournet Natalia Kulatova Tahina Ramananandro Aseem Rastogi Nikhil Swamy Christoph M. Wintersteiger and Santiago Zanella-Beguelin. 2020. EverCrypt: A Fast Verified Cross-Platform Cryptographic Provider. In 2020 IEEE Symposium on Security and Privacy (SP). 983\u20131002. doi:10.1109\/SP40000.2020.00114","DOI":"10.1109\/SP40000.2020.00114"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","unstructured":"Chaiyong Ragkhitwetsagul and Jens Krinke. 2019. Siamese: scalable and incremental code clone search via multiple code representations. Empirical Software Engineering (2019) 1\u201349. https:\/\/doi.org\/10.1007\/s10664-019-09697-7 10.1007\/s10664-019-09697-7","DOI":"10.1007\/s10664-019-09697-7"},{"key":"e_1_3_1_52_1","first-page":"1465","volume-title":"Proceedings of the 28th USENIX Conference on Security Symposium (Santa Clara, CA, USA) (SEC\u201919)","author":"Ramananandro Tahina","year":"2019","unstructured":"Tahina Ramananandro, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. 2019. Everparse: verified secure zero-copy parsers for authenticated message formats. In Proceedings of the 28th USENIX Conference on Security Symposium (Santa Clara, CA, USA) (SEC\u201919). USENIX Association, USA, 1465\u20131482. https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/delignat-lavaud"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","unstructured":"Chanchal K. Roy and James R. Cordy. 2008. NICAD: Accurate Detection of Near-Miss Intentional Clones Using Flexible Pretty-Printing and Code Normalization. In 2008 16th IEEE International Conference on Program Comprehension. 172\u2013181. doi:10.1109\/ICPC.2008.41","DOI":"10.1109\/ICPC.2008.41"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3644033.3644374"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2022.acl-long.60"},{"key":"e_1_3_1_56_1","doi-asserted-by":"crossref","unstructured":"Hongjin SU Jungo Kasai Chen Henry Wu Weijia Shi Tianlu Wang Jiayi Xin Rui Zhang Mari Ostendorf Luke Zettlemoyer Noah A. Smith and Tao Yu. 2023. Selective Annotation Makes Language Models Better Few-Shot Learners. In The Eleventh International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=qY1hlv7gwg","DOI":"10.1109\/ICASSP49357.2023.10095738"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65112-0_7"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","unstructured":"Nikhil Swamy C\u0103t\u0103lin Hri\u0163cu Chantal Keller Aseem Rastogi Antoine Delignat-Lavaud Simon Forest Karthikeyan Bhargavan C\u00e9dric Fournet Pierre-Yves Strub Markulf Kohlweiss Jean-Karim Zinzindohoue and Santiago Zanella-B\u00e9guelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/2837614.2837655 10.1145\/2837614.2837655","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","unstructured":"Rajkumar Tekchandani Rajesh Kumar Bhatia and Maninder Singh. 2013. Semantic code clone detection using parse trees and grammar recovery. In Confluence 2013: The Next Generation Information Technology Summit (4th International Conference). 41\u201346. doi:10.1049\/cp.2013.2291","DOI":"10.1049\/cp.2013.2291"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","unstructured":"Dethe Tukaram and Uma Maheswari B. 2019. Design and Development of Software Tool for Code Clone Search Detection and Analysis. In 2019 3rd International conference on Electronics Communication and Aerospace Technology (ICECA). 1002\u20131006. doi:10.1109\/ICECA.2019.8821928","DOI":"10.1109\/ICECA.2019.8821928"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11042-018-5827-6"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","unstructured":"Niki Vazou Eric L. Seidel and Ranjit Jhala. 2014. LiquidHaskell: experience with refinement types in the real world. In Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell. doi:10.1145\/2633357.2633366","DOI":"10.1145\/2633357.2633366"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","unstructured":"Robert A. Wagner and Michael J. Fischer. 1974. The String-to-String Correction Problem. (1974). https:\/\/doi.org\/10.1145\/321796.321811 10.1145\/321796.321811","DOI":"10.1145\/321796.321811"},{"key":"e_1_3_1_64_1","unstructured":"Haiming Wang Huajian Xin Chuanyang Zheng Zhengying Liu Qingxing Cao Yinya Huang Jing Xiong Han Shi Enze Xie Jian Yin Zhenguo Li and Xiaodan Liang. 2024. LEGO-Prover: Neural Theorem Proving with Growing Libraries. In The Twelfth International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=3f5PALef5B"},{"key":"e_1_3_1_65_1","unstructured":"Jason Wei Xuezhi Wang Dale Schuurmans Maarten Bosma Brian Ichter Fei Xia Ed H. Chi Quoc V. Le and Denny Zhou. [n. d.]. Chain-of-thought prompting elicits reasoning in large language models (NIPS \u201922). https:\/\/dl.acm.org\/doi\/10.5555\/3600270.3602070"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","unstructured":"Chunqiu Steven Xia Yuxiang Wei and Lingming Zhang. 2023. Automated Program Repair in the Era of Large Pretrained Language Models. In 2023 IEEE\/ACM 45th International Conference on Software Engineering (ICSE). 1482\u20131494. doi:10.1109\/ICSE48619.2023.00129","DOI":"10.1109\/ICSE48619.2023.00129"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","unstructured":"Chunqiu Steven Xia and Lingming Zhang. 2024. Automated Program Repair via Conversation: Fixing 162 out of 337 Bugs for $0.42 Each using ChatGPT. In Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis. doi:10.1145\/3650212.3680323","DOI":"10.1145\/3650212.3680323"},{"key":"e_1_3_1_68_1","unstructured":"Chenyuan Yang Xuheng Li Md Rakib Hossain Misu Jianan Yao Weidong Cui Yeyun Gong Chris Hawblitzel Shuvendu Lahiri Jacob R. Lorch Shuai Lu Fan Yang Ziqiao Zhou and Shan Lu. 2024. AutoVerus: Automated Proof Generation for Rust Code. arXiv:2409.13082 [cs.SE] https:\/\/arxiv.org\/abs\/2409.13082"},{"key":"e_1_3_1_69_1","unstructured":"Kaiyu Yang and Jia Deng. 2019. Learning to Prove Theorems via Interacting with Proof Assistants. arXiv:1905.09381 [cs.LO] https:\/\/arxiv.org\/abs\/1905.09381"},{"key":"e_1_3_1_70_1","unstructured":"Kaiyu Yang Aidan M. Swope Alex Gu Rahul Chalamala Peiyang Song Shixing Yu Saad Godil Ryan J. Prenger and Animashree Anandkumar. 2023a. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. In NeurIPS 2023. http:\/\/papers.nips.cc\/paper_files\/paper\/2023\/hash\/4441469427094f8873d0fecb0c4e1cee-Abstract-Datasets_and_Benchmarks.html"},{"key":"e_1_3_1_71_1","unstructured":"Zhenkun Yang Wen Wang Jeremy Casas Pasquale Cocchini and Jin Yang. 2023b. Towards A Correct-by-Construction FHE Model. Cryptology ePrint Archive. https:\/\/eprint.iacr.org\/2023\/281"},{"key":"e_1_3_1_72_1","doi-asserted-by":"publisher","unstructured":"Yaoshen Yu Zhiqiu Huang Guohua Shen Weiwei Li and Yichao Shao. 2022. ASTENS-BWA: Searching partial syntactic similar regions between source code fragments via AST-based encoded sequence alignment. Sci. Comput. Program. (2022). doi:10.1016\/j.scico.2022.102839","DOI":"10.1016\/j.scico.2022.102839"},{"key":"e_1_3_1_73_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2023.111796"},{"key":"e_1_3_1_74_1","unstructured":"Stefan Zetzsche and Jean-Baptiste Tristan. 2023. Dafny-VMC: a Library for Verified Monte Carlo Algorithms. https:\/\/github.com\/dafny-lang\/Dafny-VMC"},{"key":"e_1_3_1_75_1","doi-asserted-by":"publisher","DOI":"10.1137\/0218082"},{"key":"e_1_3_1_76_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxs018"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720499","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720499","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:28:33Z","timestamp":1787588913000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720499"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":75,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720499"],"URL":"https:\/\/doi.org\/10.1145\/3720499","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}