{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:40:45Z","timestamp":1780994445236,"version":"3.54.1"},"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\/"}],"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 , a tool that alleviates this burden by automatically generating assertions using large language models (LLMs).  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 , a dataset of complex lemmas we extracted from three real-world Dafny codebases. Our evaluation shows that is able to generate over 56.6% 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":6,"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_2_1_1_1","unstructured":"2023. Verification Optimization. https:\/\/dafny.org\/latest\/VerificationOptimization\/VerificationOptimization"},{"key":"e_1_2_1_2_1","unstructured":"2024. AWS Encryption SDK for Dafny. https:\/\/github.com\/aws\/aws-encryption-sdk-dafny"},{"key":"e_1_2_1_3_1","unstructured":"2024. Cedar. https:\/\/www.cedarpolicy.com\/"},{"key":"e_1_2_1_4_1","unstructured":"2024. Dafny-libraries. https:\/\/github.com\/dafny-lang\/libraries"},{"key":"e_1_2_1_5_1","unstructured":"2024. GPT-4o. https:\/\/platform.openai.com\/docs\/models\/gpt-4o"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","unstructured":"Wolfgang Ahrendt Bernhard Beckert Richard Bubel Reiner H\u00e4hnle Peter H. Schmitt and Mattias Ulbrich (Eds.). 2016. Deductive Software Verification - The KeY Book - From Theory to Practice. Springer. https:\/\/doi.org\/10.1007\/978-3-319-49812-6 10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290353"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_2_1_9_1","volume-title":"Program Synthesis with Large Language Models. CoRR, abs\/2108.07732","author":"Austin Jacob","year":"2021","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. arxiv:2108.07732"},{"key":"e_1_2_1_10_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.). https:\/\/doi.org\/10.18653\/v1\/2024.findings-naacl.41 10.18653\/v1\/2024.findings-naacl.41","DOI":"10.18653\/v1\/2024.findings-naacl.41"},{"key":"e_1_2_1_11_1","volume-title":"Jianang Yang, William E. Byrd, Robert Zinkov, and Nada Amin.","author":"Brandfonbrener David","year":"2024","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. arxiv:2402.08147"},{"key":"e_1_2_1_12_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 \u201920. isbn:9781713829546 https:\/\/dl.acm.org\/doi\/abs\/10.5555\/3495724.3495883"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_32"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE55347.2025.00002"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2023.findings-emnlp.614"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-015-1573-7"},{"key":"e_1_2_1_17_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. https:\/\/doi.org\/10.48550\/arXiv.2107.03374 arxiv:2107.03374. 10.48550\/arXiv.2107.03374","DOI":"10.48550\/arXiv.2107.03374"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSME55016.2022.00080"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSEC.2022.3153035"},{"key":"e_1_2_1_22_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.). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8 10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616243"},{"key":"e_1_2_1_24_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_2_1_25_1","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. isbn:978-1-931971-16-4 https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/hawblitzel"},{"key":"e_1_2_1_26_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.). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2 10.1007\/978-3-642-39799-8_2","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.30"},{"key":"e_1_2_1_28_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. arxiv:2311.07948"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2020.emnlp-main.550"},{"key":"e_1_2_1_30_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_2_1_31_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_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_2_1_34_1","unstructured":"K. Rustan M. Leino. 2008. This is Boogie 2. Microsoft Research. https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2\/"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_36_1","volume-title":"Saxe","author":"Leino K. Rustan M.","year":"2005","unstructured":"K. Rustan M. Leino, Todd Millstein, and James B. Saxe. 2005. Generating error traces from verification-condition counterexamples. Science of Computer Programming, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0167642304001510"},{"key":"e_1_2_1_37_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. arxiv:2404.09939"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2022.deelio-1.10"},{"key":"e_1_2_1_39_1","volume-title":"Nada Amin, and Max Tegmark.","author":"Loughridge Chloe","year":"2024","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. arxiv:2406.08467"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2022.acl-long.556"},{"key":"e_1_2_1_41_1","volume-title":"The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS\u201923","author":"Maciej Miku\u0142","year":"2023","unstructured":"Maciej Miku\u0142 a, Szymon Antoniak, Szymon Tworkowski, Bartosz Piotrowski, Albert Jiang, Jin Peng Zhou, Christian Szegedy, \u0141 ukasz Kuci\u0144ski, Piotr Mi\u0142 o\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_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3643763"},{"key":"e_1_2_1_43_1","volume-title":"Ranjit Jhala, Nadia Polikarpova, and Yuanyuan Zhou.","author":"Mugnier Eric","year":"2024","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. arxiv:2405.16792"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.14676571"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.14676571"},{"key":"e_1_2_1_46_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. arxiv:2201.10005"},{"key":"e_1_2_1_47_1","volume-title":"ICML","author":"Pei Kexin","year":"2023","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_2_1_48_1","doi-asserted-by":"publisher","unstructured":"Lutz Prechelt and Michael Phlippsen. 2000. JPlag: Finding plagiarisms among a set of programs. https:\/\/doi.org\/10.5445\/IR\/542000 10.5445\/IR\/542000","DOI":"10.5445\/IR\/542000"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00114"},{"key":"e_1_2_1_50_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 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_2_1_51_1","volume-title":"Proceedings of the 28th USENIX Conference on Security Symposium (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 (SEC\u201919). USENIX Association, USA. 1465\u20131482. isbn:9781939133069 https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/delignat-lavaud"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPC.2008.41"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3644033.3644374"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2022.acl-long.60"},{"key":"e_1_2_1_55_1","volume-title":"Selective Annotation Makes Language Models Better Few-Shot Learners. In The Eleventh International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=qY1hlv7gwg","author":"Jungo Kasai Hongjin SU","year":"2023","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"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65112-0_7"},{"key":"e_1_2_1_57_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_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1049\/cp.2013.2291"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECA.2019.8821928"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11042-018-5827-6"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633366"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/321796.321811"},{"key":"e_1_2_1_63_1","volume-title":"LEGO-Prover: Neural Theorem Proving with Growing Libraries. In The Twelfth International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=3f5PALef5B","author":"Wang Haiming","year":"2024","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_2_1_64_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. isbn:9781713871088 https:\/\/dl.acm.org\/doi\/10.5555\/3600270.3602070"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00129"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3650212.3680323"},{"key":"e_1_2_1_67_1","volume-title":"Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, and Shan Lu.","author":"Yang Chenyuan","year":"2024","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. arxiv:2409.13082"},{"key":"e_1_2_1_68_1","unstructured":"Kaiyu Yang and Jia Deng. 2019. Learning to Prove Theorems via Interacting with Proof Assistants. arxiv:1905.09381. arxiv:1905.09381"},{"key":"e_1_2_1_69_1","volume-title":"NeurIPS","author":"Yang Kaiyu","year":"2023","unstructured":"Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. 2023. 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_2_1_70_1","unstructured":"Zhenkun Yang Wen Wang Jeremy Casas Pasquale Cocchini and Jin Yang. 2023. Towards A Correct-by-Construction FHE Model. Cryptology ePrint Archive. https:\/\/eprint.iacr.org\/2023\/281"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2022.102839"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2023.111796"},{"key":"e_1_2_1_73_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_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1137\/0218082"},{"key":"e_1_2_1_75_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":[[2025,10,9]],"date-time":"2025-10-09T17:06:40Z","timestamp":1760029600000},"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"}}]}}