---
title: "Clover: Closed-Loop Verifiable Code Generation (2024)"
description: "LLMs can now write code, but nothing reliably confirms that the output does what was intended. 75 references, cited by 14 papers here."
authors: ["Chuyue Sun", "Ying Sheng", "Oded Padon", "Clark Barrett"]
year: 2024
venue: "arXiv:2310.17807"
source: "https://arxiv.org/abs/2310.17807"
doi: "10.48550/arxiv.2310.17807"
arxiv: "2310.17807"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/sun-2024-clover-closed-loop-verifiable-code/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/sun-2024-clover-closed-loop-verifiable-code/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2024](https://md.research.elamur.ai/free/en/papers/2024/page/8/) / Clover: Closed-Loop Verifiable Code Generation

# Clover: Closed-Loop Verifiable Code Generation

**Authors:** [Chuyue Sun](https://md.research.elamur.ai/free/en/authors/chuyue-sun/), [Ying Sheng](https://md.research.elamur.ai/free/en/authors/ying-sheng/), [Oded Padon](https://md.research.elamur.ai/free/en/authors/oded-padon/) and [Clark Barrett](https://md.research.elamur.ai/free/en/authors/clark-barrett/) · **Year:** 2024 · **Venue:** [arXiv:2310.17807](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/) ([Lecture notes in computer science 2024](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/2024/)) · **Publisher:** [Springer Science+Business Media](https://md.research.elamur.ai/free/en/publishers/springer-science-business-media/) · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/2310.17807) · [PDF](https://arxiv.org/pdf/2310.17807) · [DOI 10.48550/arxiv.2310.17807](https://doi.org/10.48550/arxiv.2310.17807) · [arXiv 2310.17807](https://arxiv.org/abs/2310.17807) · [OpenAlex](https://openalex.org/W4400675892)

**Citations:** 42 citations (OpenAlex, 2026-10-14) · [14](https://md.research.elamur.ai/free/en/papers/sun-2024-clover-closed-loop-verifiable-code/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary

LLMs can now write code, but nothing reliably confirms that the output does what was intended. Clover (Closed-Loop Verifiable Code Generation) addresses this by treating correctness checking as a consistency problem. Each generated artifact must contain three parts: code, formal annotations (pre/postconditions, loop invariants) and a natural-language docstring. Clover then runs six checks across these parts. The Dafny verifier handles the formal steps, and GPT-4 handles reconstruction, for example rebuilding annotations from the docstring and comparing them with the originals.

To test the idea, the authors built CloverBench, a hand-made set of 60 textbook-level Dafny programs. It contains correct examples plus deliberately broken variants. The checker accepted up to 87% of correct programs and let no adversarial incorrect program through. On the human-written MBPP-DFY-50 set it exposed 6 faulty programs. A smaller Verus/Rust trial indicates the approach can move to other verification tools. The work matters because it points toward generated code that comes with machine-checked guarantees instead of relying on human review.

## Key points

- The six Clover checks are anno-sound, anno-complete, doc2anno, anno2doc, code2doc and doc2code. They were implemented with GPT-4 and the Dafny verifier.
- CloverBench consists of 60 hand-crafted Dafny examples with docstrings, including adversarial incorrect variants. Results: 87% acceptance of ground-truth examples, 100% rejection of incorrect ones (zero false positives).
- doc2anno rejected incorrect examples most often, because Dafny formally checks whether the two sets of annotations are logically equivalent.
- On MBPP-DFY-50, Clover detected 6 incorrect programs and accepted 89% of the correct ones.
- In a preliminary Verus study on 41 ground-truth examples, Clover accepted 32 with k=1 and 36 with k=10.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Stanford University](https://md.research.elamur.ai/free/en/universities/stanford-university/) — University, Stanford, United States · 567 works · 335,189 citations
- [VMware](https://md.research.elamur.ai/free/en/companies/vmware/) — Company, Palo Alto, United States · 3 works · 56 citations

📚 Shelves (4): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🗄️ Information Systems](https://md.research.elamur.ai/free/en/shelves/computer-science/information-systems/) · 1,888 works · [💻 Software](https://md.research.elamur.ai/free/en/shelves/computer-science/software/) · 150 works

🧭 Topics (1): [💻 Code & programming languages](https://md.research.elamur.ai/free/en/topics/code-and-programming/) · 194 works

## Cite

Cite as: Chuyue Sun, Ying Sheng, Oded Padon and Clark Barrett. 2024. Clover: Closed-Loop Verifiable Code Generation. arXiv:2310.17807.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{sun2024clover,
  title = {{Clover: Closed-Loop Verifiable Code Generation}},
  author = {Chuyue Sun, Ying Sheng, Oded Padon and Clark Barrett},
  year = {2024},
  doi = {10.48550/arxiv.2310.17807},
  eprint = {2310.17807},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2310.17807}
}
```

- [← previous Unintended Impacts of LLM Alignment on Global Representation](https://md.research.elamur.ai/free/en/papers/ryan-2024-unintended-impacts-llm-alignment-global/)
- [next → Massively Multi-Cultural Knowledge Acquisition & LM Benchmarking](https://md.research.elamur.ai/free/en/papers/fung-2024-massively-multi-cultural-knowledge-acquisition/)
- [↑ back to papers of 2024](https://md.research.elamur.ai/free/en/papers/2024/page/8/)

## References

75 references, 26 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Rajeev Alur et al. “[Syntax-guided synthesis](https://md.research.elamur.ai/free/en/papers/alur-2013-syntax-guided-synthesis/)”. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. IEEE, 2013, pp. 1–8. url: [https://ieeexplore.ieee.org/document/6679385/](https://ieeexplore.ieee.org/document/6679385/). [↗](https://ieeexplore.ieee.org/document/6679385/)
2. Jacob Austin et al. “[Program Synthesis with Large Language Models](https://md.research.elamur.ai/free/en/papers/austin-2021-program-synthesis-large-language-models/)”. In: CoRR abs/2108.07732 (2021). arXiv: 2108.07732. url: https://arxiv.org/abs/2108.07732. [↗](https://arxiv.org/abs/2108.07732)
3. John Barnes. SPARK: The Proven Approach to High Integrity Software. Altran Praxis, 2012. [find](https://scholar.google.com/scholar?q=John+Barnes%2E+SPARK%3A+The+Proven+Approach+to+High+Integrity+Software%2E+Altran+Praxis%2C+2012%2E)
4. Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfiability. Vol. 185. IOS press, 2009. [find](https://scholar.google.com/scholar?q=Armin+Biere%2C+Marijn+Heule%2C+and+Hans+van+Maaren%2E+Handbook+of+satisfiability%2E+Vol%2E+185%2E+IOS+press%2C+2009%2E)
5. Matthew Bowers et al. “Top-Down Synthesis for Library Learning”. In: Proc. ACM Program. Lang. 7.POPL (2023), pp. 1182–1213. doi: 10.1145/3571234. url: https://doi.org/10.1145/3571234. [↗](https://doi.org/10.1145/3571234)
6. David Brandfonbrener et al. “Verified Multi-Step Synthesis using Large Language Models and Monte Carlo Tree Search”. In: arXiv preprint arXiv:2402.08147 (2024). — [arXiv:2402.08147](https://arxiv.org/abs/2402.08147) [find](https://scholar.google.com/scholar?q=David+Brandfonbrener+et+al%2E+%E2%80%9CVerified+Multi%2DStep+Synthesis+using+Large+Language+Models+and+Monte+Carlo+Tree+Search%E2%80%9D%2E+In%3A+arXiv+preprint+arXiv%3A2402%2E08147+%282024%29%2E+%E2%80%94+%5BarXiv%3A2402%2E08147%5D%28https%3A%2F%2Farxiv%2Eorg%2F)
7. Sébastien Bubeck et al. “[Sparks of artificial general intelligence: Early experiments with gpt-4](https://md.research.elamur.ai/free/en/papers/bubeck-2023-sparks-artificial-general-intelligence-early/)”. In: arXiv preprint arXiv:2303.12712 (2023).
8. Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. “KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs”. In: 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings. Ed.… [find](https://scholar.google.com/scholar?q=Cristian+Cadar%2C+Daniel+Dunbar%2C+and+Dawson+R%2E+Engler%2E+%E2%80%9CKLEE%3A+Unassisted+and+Automatic+Generation+of+High%2DCoverage+Tests+for+Complex+Systems+Programs%E2%80%9D%2E+In%3A+8th+USENIX+Symposium+on+Operating+Systems+Desi)
9. Cristian Cadar and Koushik Sen. “Symbolic execution for software testing: three decades later”. In: Commun. ACM 56.2 (2013), pp. 82–90. doi: 10.1145/2408776.2408795. url: https://doi.org/10.1145/2408776.2408795. — [doi:10.1145/2408776.2408795](https://doi.org/10.1145/2408776.2408795) [↗](https://doi.org/10.1145/2408776.2408795)
10. Yiannis Charalambous et al. “A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification”. In: CoRR abs/2305.14752 (2023). doi: 10 . 48550 / arXiv . 2305 . 14752. arXiv: 2305.14752. url: https://doi.org/10.48550/arXiv.2305.14752. — [doi:10.48550/arxiv.2305.14752](https://doi.org/10.48550/arxiv.2305.14752) [↗](https://doi.org/10.48550/arXiv.2305.14752)
11. Swarat Chaudhuri et al. “Neurosymbolic Programming”. In: Found. Trends Program. Lang. 7.3 (2021), pp. 158–243. doi: 10.1561/2500000049. url: https://doi.org/10.1561/2500000049. — [doi:10.1561/2500000049](https://doi.org/10.1561/2500000049) [↗](https://doi.org/10.1561/2500000049)
12. Bei Chen et al. “CodeT: Code Generation with Generated Tests”. In: The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. url: [https://openreview.net/pdf?id=ktrw68Cmu9c](https://openreview.net/pdf?id=ktrw68Cmu9c). [↗](https://openreview.net/pdf?id=ktrw68Cmu9c)
13. Bei Chen et al. “Codet: Code generation with generated tests”. In: arXiv preprint arXiv:2207.10397 (2022). Chuyue Sun, Ying Sheng, Oded Padon, Clark Barrett [find](https://scholar.google.com/scholar?q=Bei+Chen+et+al%2E+%E2%80%9CCodet%3A+Code+generation+with+generated+tests%E2%80%9D%2E+In%3A+arXiv+preprint+arXiv%3A2207%2E10397+%282022%29%2E+Chuyue+Sun%2C+Ying+Sheng%2C+Oded+Padon%2C+Clark+Barrett)
14. Mark Chen et al. “[Evaluating Large Language Models Trained on Code](https://md.research.elamur.ai/free/en/papers/chen-2021-evaluating-large-language-models-trained/)”. In: CoRR abs/2107.03374 (2021). arXiv: 2107 . 03374. url: https://arxiv.org/abs/2107.03374. [↗](https://arxiv.org/abs/2107.03374)
15. Xinyun Chen et al. “Teaching large language models to self-debug”. In: arXiv preprint arXiv:2304.05128 (2023). [find](https://scholar.google.com/scholar?q=Xinyun+Chen+et+al%2E+%E2%80%9CTeaching+large+language+models+to+self%2Ddebug%E2%80%9D%2E+In%3A+arXiv+preprint+arXiv%3A2304%2E05128+%282023%29%2E)
16. Zhoujun Cheng et al. “[Binding Language Models in Symbolic Languages](https://md.research.elamur.ai/free/en/papers/cheng-2022-binding-language-models-symbolic-languages/)”. In: The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. url: [https://openreview.net/pdf?id=lH1PV42cbF](https://openreview.net/pdf?id=lH1PV42cbF). [↗](https://openreview.net/pdf?id=lH1PV42cbF)
17. Aakanksha Chowdhery et al. “[PaLM: Scaling Language Modeling with Pathways](https://md.research.elamur.ai/free/en/papers/chowdhery-2022-palm-scaling-language-modeling-pathways/)”. In: CoRR abs/2204.02311 (2022). doi: 10 . 48550 / arXiv . 2204 . 02311. arXiv: 2204 . 02311. url: https://doi.org/10 . 48550 / arXiv.2204.02311.
18. Berkeley R. Churchill et al. “Semantic program alignment for equivalence checking”. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019. Ed. by Kathryn S. McKinley and Kathleen Fisher. ACM, 2019, pp. 1027… — [doi:10.1145/3314221.3314596](https://doi.org/10.1145/3314221.3314596) [find](https://scholar.google.com/scholar?q=Berkeley+R%2E+Churchill+et+al%2E+%E2%80%9CSemantic+program+alignment+for+equivalence+checking%E2%80%9D%2E+In%3A+Proceedings+of+the+40th+ACM+SIGPLAN+Conference+on+Programming+Language+Design+and+Implementation%2C+PLDI+2019%2C+Pho)
19. Karl Cobbe et al. “[Training Verifiers to Solve Math Word Problems](https://md.research.elamur.ai/free/en/papers/cobbe-2021-training-verifiers-solve-math-word/)”. In: CoRR abs/2110.14168 (2021). arXiv: 2110.14168. url: https://arxiv.org/abs/2110.14168. [↗](https://arxiv.org/abs/2110.14168)
20. Domenico Cotroneo et al. “Vulnerabilities in AI Code Generators: Exploring Targeted Data Poisoning Attacks”. In: CoRR abs/2308.04451 (2023). doi: 10 . 48550 / arXiv . 2308 . 04451. arXiv: 2308 . 04451. url: https : //doi.org/10.48550/arXiv.2308.04451. — [doi:10.48550/arxiv.2308.04451](https://doi.org/10.48550/arxiv.2308.04451) [find](https://scholar.google.com/scholar?q=Domenico+Cotroneo+et+al%2E+%E2%80%9CVulnerabilities+in+AI+Code+Generators%3A+Exploring+Targeted+Data+Poisoning+Attacks%E2%80%9D%2E+In%3A+CoRR+abs%2F2308%2E04451+%282023%29%2E+doi%3A+10+%2E+48550+%2F+arXiv+%2E+2308+%2E+04451%2E+arXiv%3A+2308+%2E+04451)
21. Yangruibo Ding et al. “TRACED: Execution-aware Pre-training for Source Code”. In: arXiv preprint arXiv:2306.07487 (2023). — [arXiv:2306.07487](https://arxiv.org/abs/2306.07487) [find](https://scholar.google.com/scholar?q=Yangruibo+Ding+et+al%2E+%E2%80%9CTRACED%3A+Execution%2Daware+Pre%2Dtraining+for+Source+Code%E2%80%9D%2E+In%3A+arXiv+preprint+arXiv%3A2306%2E07487+%282023%29%2E+%E2%80%94+%5BarXiv%3A2306%2E07487%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2306%2E07487%29)
22. Kevin Ellis et al. “DreamCoder: bootstrapping inductive program synthesis with wake-sleep library learning”. In: PLDI ’21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021. Ed. by Stephen N. Freund and Eran Yahav. AC… — [doi:10.1145/3453483.3454080](https://doi.org/10.1145/3453483.3454080) [find](https://scholar.google.com/scholar?q=Kevin+Ellis+et+al%2E+%E2%80%9CDreamCoder%3A+bootstrapping+inductive+program+synthesis+with+wake%2Dsleep+library+learning%E2%80%9D%2E+In%3A+PLDI+%E2%80%9921%3A+42nd+ACM+SIGPLAN+International+Conference+on+Programming+Language+Design+and+)
23. Robert W. Floyd. “Assigning Meanings to Programs”. In: Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics. American Mathematical Society, 1967, pp. 19–32. [find](https://scholar.google.com/scholar?q=Robert+W%2E+Floyd%2E+%E2%80%9CAssigning+Meanings+to+Programs%E2%80%9D%2E+In%3A+Mathematical+Aspects+of+Computer+Science%2C+Proceedings+of+Symposia+in+Applied+Mathematics%2E+American+Mathematical+Society%2C+1967%2C+pp%2E+19%E2%80%9332%2E)
24. Sayontan Ghosh et al. “SpecNFS: A Challenge Dataset Towards Extracting Formal Models from Natural Language Specifications”. In: Proceedings of the Thirteenth Language Resources and Evaluation Conference, LREC 2022, Marseille, France, 20-25 June 2022. Ed. by Nicoletta Calzolari et al. European Langua… [find](https://scholar.google.com/scholar?q=Sayontan+Ghosh+et+al%2E+%E2%80%9CSpecNFS%3A+A+Challenge+Dataset+Towards+Extracting+Formal+Models+from+Natural+Language+Specifications%E2%80%9D%2E+In%3A+Proceedings+of+the+Thirteenth+Language+Resources+and+Evaluation+Conferen)
25. Github Copilot. Github Copilot: Your AI Pair Programmer. [https://github.com/features/copilot](https://github.com/features/copilot). Clover: Closed-Loop Verifiable Code Generation [↗](https://github.com/features/copilot)
26. Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. “[Program Synthesis](https://md.research.elamur.ai/free/en/papers/gulwani-2017-program-synthesis/)”. In: Found. Trends Program. Lang. 4.1-2 (2017), pp. 1–119. doi: 10.1561/2500000010. url: https://doi.org/10.1561/2500000010. [↗](https://doi.org/10.1561/2500000010)
27. Christopher Hahn et al. “Formal Specifications from Natural Language”. In: CoRR abs/2206.01962 (2022). doi: 10 . 48550 / arXiv . 2206 . 01962. arXiv: 2206 . 01962. url: https://doi.org/10 . 48550 / arXiv. 2206 . 01962. — [arXiv:2206.01962](https://arxiv.org/abs/2206.01962) [find](https://scholar.google.com/scholar?q=Christopher+Hahn+et+al%2E+%E2%80%9CFormal+Specifications+from+Natural+Language%E2%80%9D%2E+In%3A+CoRR+abs%2F2206%2E01962+%282022%29%2E+doi%3A+10+%2E+48550+%2F+arXiv+%2E+2206+%2E+01962%2E+arXiv%3A+2206+%2E+01962%2E+url%3A+https%3A%2F%2Fdoi%2Eorg%2F10+%2E+48550+%2F+ar)
28. James Hendler. “Understanding the limits of AI coding”. In: Science 379.6632 (2023), pp. 548–548. [find](https://scholar.google.com/scholar?q=James+Hendler%2E+%E2%80%9CUnderstanding+the+limits+of+AI+coding%E2%80%9D%2E+In%3A+Science+379%2E6632+%282023%29%2C+pp%2E+548%E2%80%93548%2E)
29. Dan Hendrycks et al. “[Measuring Coding Challenge Competence With APPS](https://md.research.elamur.ai/free/en/papers/hendrycks-2021-measuring-coding-challenge-competence-apps/)”. In: Proceedings of the Neural Information Processing Systems Track on Datasets and Benchmarks 1, NeurIPS Datasets and Benchmarks 2021, December 2021, virtual. Ed. by Joaquin Vanschoren and Sai-Kit Yeung. 2021. url: https://datas…
30. C. A. R. Hoare. “An Axiomatic Basis for Computer Programming”. In: Commun. ACM 12.10 (1969), pp. 576–580. doi: 10.1145/363235.363259. url: [http://doi.acm.org/10.1145/363235.363259](http://doi.acm.org/10.1145/363235.363259). — [doi:10.1145/363235.363259](https://doi.org/10.1145/363235.363259) [↗](http://doi.acm.org/10.1145/363235.363259)
31. Jeevana Priya Inala et al. “[Fault-Aware Neural Code Rankers](https://md.research.elamur.ai/free/en/papers/inala-2022-fault-aware-neural-code-rankers/)”. In: NeurIPS. 2022. url: [http://papers.nips.cc/paper%5C_files/paper/2022/hash/5762c579d09811b7639be2389b3d07be-Abstract-Conference.html](http://papers.nips.cc/paper%5C_files/paper/2022/hash/5762c579d09811b7639be2389b3d07be-Abstract-Conference.html). [↗](http://papers.nips.cc/paper%5C_files/paper/2022/hash/5762c579d09811b7639be2389b3d07be-Abstract-Conference.html)
32. Darren Key, Wen-Ding Li, and Kevin Ellis. “I Speak, You Verify: Toward Trustworthy Neural Program Synthesis”. In: CoRR abs/2210.00848 (2022). doi: 10 . 48550 / arXiv . 2210 . 00848. arXiv: 2210 . 00848. url: https://doi.org/10.48550/arXiv.2210.00848. — [doi:10.48550/arxiv.2210.00848](https://doi.org/10.48550/arxiv.2210.00848) [↗](https://doi.org/10.48550/arXiv.2210.00848)
33. James C. King. “Symbolic Execution and Program Testing”. In: Commun. ACM 19.7 (1976), pp. 385–394. doi: 10.1145/360248.360252. url: https://doi.org/10.1145/360248.360252. — [doi:10.1145/360248.360252](https://doi.org/10.1145/360248.360252) [↗](https://doi.org/10.1145/360248.360252)
34. Yuhang Lai et al. “DS-1000: A Natural and Reliable Benchmark for Data Science Code Generation”. In: International Conference on Machine Learning, ICML 2023, 23-29 July 2023, Honolulu, Hawaii, USA. Ed. by Andreas Krause et al. Vol. 202. Proceedings of Machine Learning Research. PMLR, 2023, pp. 18319–… [find](https://scholar.google.com/scholar?q=Yuhang+Lai+et+al%2E+%E2%80%9CDS%2D1000%3A+A+Natural+and+Reliable+Benchmark+for+Data+Science+Code+Generation%E2%80%9D%2E+In%3A+International+Conference+on+Machine+Learning%2C+ICML+2023%2C+23%2D29+July+2023%2C+Honolulu%2C+Hawaii%2C+USA%2E+Ed%2E)
35. Andrea Lattuada et al. Verus: Verifying Rust Programs using Linear Ghost Types (extended version). 2023. arXiv: 2303.05491 [cs.LO]. [find](https://scholar.google.com/scholar?q=Andrea+Lattuada+et+al%2E+Verus%3A+Verifying+Rust+Programs+using+Linear+Ghost+Types+%28extended+version%29%2E+2023%2E+arXiv%3A+2303%2E05491+%5Bcs%2ELO%5D%2E)
36. K Rustan M Leino. “Dafny: An automatic program verifier for functional correctness”. In: International conference on logic for programming artificial intelligence and reasoning. Springer. 2010, pp. 348–370. [find](https://scholar.google.com/scholar?q=K+Rustan+M+Leino%2E+%E2%80%9CDafny%3A+An+automatic+program+verifier+for+functional+correctness%E2%80%9D%2E+In%3A+International+conference+on+logic+for+programming+artificial+intelligence+and+reasoning%2E+Springer%2E+2010%2C+pp%2E+34)
37. Yifei Li et al. “On the Advance of Making Language Models Better Reasoners”. In: CoRR abs/2206.02336 (2022). doi: 10.48550/arXiv.2206.02336. arXiv: 2206.02336. url: https://doi.org/10.48550/arXiv.2206.02336. Chuyue Sun, Ying Sheng, Oded Padon, Clark Barrett — [doi:10.48550/arxiv.2206.02336](https://doi.org/10.48550/arxiv.2206.02336) [↗](https://doi.org/10.48550/arXiv.2206.02336)
38. Yujia Li et al. “[Competition-level code generation with alphacode](https://md.research.elamur.ai/free/en/papers/li-2022-competition-level-code-generation-alphacode/)”. In: Science 378.6624 (2022), pp. 1092–1097.
39. Chang Liu et al. “Towards General Loop Invariant Generation via Coordinating Symbolic Execution and Large Language Models”. In: arXiv preprint arXiv:2311.10483 (2023). — [arXiv:2311.10483](https://arxiv.org/abs/2311.10483) [find](https://scholar.google.com/scholar?q=Chang+Liu+et+al%2E+%E2%80%9CTowards+General+Loop+Invariant+Generation+via+Coordinating+Symbolic+Execution+and+Large+Language+Models%E2%80%9D%2E+In%3A+arXiv+preprint+arXiv%3A2311%2E10483+%282023%29%2E+%E2%80%94+%5BarXiv%3A2311%2E10483%5D%28https%3A%2F%2Farx)
40. Jiawei Liu et al. “[Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://md.research.elamur.ai/free/en/papers/liu-2023-your-code-generated-chatgpt-really/)”. In: CoRR abs/2305.01210 (2023). doi: 10.48550/arXiv.2305.01210. arXiv: 2305.01210. url: https://doi.org/10.48550/arXiv.2305.01210. [↗](https://doi.org/10.48550/arXiv.2305.01210)
41. Aman Madaan et al. “Self-refine: Iterative refinement with self-feedback”. In: Advances in Neural Information Processing Systems 36 (2024). [find](https://scholar.google.com/scholar?q=Aman+Madaan+et+al%2E+%E2%80%9CSelf%2Drefine%3A+Iterative+refinement+with+self%2Dfeedback%E2%80%9D%2E+In%3A+Advances+in+Neural+Information+Processing+Systems+36+%282024%29%2E)
42. Zohar Manna and Richard Waldinger. “Knowledge and reasoning in program synthesis”. In: Artificial intelligence 6.2 (1975), pp. 175–208. [find](https://scholar.google.com/scholar?q=Zohar+Manna+and+Richard+Waldinger%2E+%E2%80%9CKnowledge+and+reasoning+in+program+synthesis%E2%80%9D%2E+In%3A+Artificial+intelligence+6%2E2+%281975%29%2C+pp%2E+175%E2%80%93208%2E)
43. Zohar Manna and Richard J Waldinger. “Toward automatic program synthesis”. In: Communications of the ACM 14.3 (1971), pp. 151–165. [find](https://scholar.google.com/scholar?q=Zohar+Manna+and+Richard+J+Waldinger%2E+%E2%80%9CToward+automatic+program+synthesis%E2%80%9D%2E+In%3A+Communications+of+the+ACM+14%2E3+%281971%29%2C+pp%2E+151%E2%80%93165%2E)
44. Md Rakib Hossain Misu et al. “[Towards AI-Assisted Synthesis of Verified Dafny Methods](https://md.research.elamur.ai/free/en/papers/misu-2024-ai-assisted-synthesis-verified-dafny/)”. In: arXiv preprint arXiv:2402.00247 (2024).
45. Nausheen Mohammed et al. “Enabling Memory Safety of C Programs using LLMs”. In: arXiv preprint arXiv:2404.01096 (2024). — [arXiv:2404.01096](https://arxiv.org/abs/2404.01096) [find](https://scholar.google.com/scholar?q=Nausheen+Mohammed+et+al%2E+%E2%80%9CEnabling+Memory+Safety+of+C+Programs+using+LLMs%E2%80%9D%2E+In%3A+arXiv+preprint+arXiv%3A2404%2E01096+%282024%29%2E+%E2%80%94+%5BarXiv%3A2404%2E01096%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2404%2E01096%29)
46. Rajdeep Mondal et al. “What do LLMs need to Synthesize Correct Router Configurations?” In: Proceedings of the 22nd ACM Workshop on Hot Topics in Networks. 2023, pp. 189–195. [find](https://scholar.google.com/scholar?q=Rajdeep+Mondal+et+al%2E+%E2%80%9CWhat+do+LLMs+need+to+Synthesize+Correct+Router+Configurations%3F%E2%80%9D+In%3A+Proceedings+of+the+22nd+ACM+Workshop+on+Hot+Topics+in+Networks%2E+2023%2C+pp%2E+189%E2%80%93195%2E)
47. Theo X Olausson et al. “[Is Self-Repair a Silver Bullet for Code Generation?](https://md.research.elamur.ai/free/en/papers/olausson-2024-self-repair-silver-bullet-code/)” In: The Twelfth International Conference on Learning Representations. 2023.
48. OpenAI. “[GPT-4 Technical Report](https://md.research.elamur.ai/free/en/papers/openai-2023-gpt-4-technical-report/)”. In: CoRR abs/2303.08774 (2023). doi: 10 . 48550 / arXiv . 2303 . 08774. arXiv: 2303 . 08774. url: https : //doi.org/10.48550/arXiv.2303.08774.
49. Liangming Pan et al. “Automatically correcting large language models: Surveying the landscape of diverse self-correction strategies”. In: arXiv preprint arXiv:2308.03188 (2023). [find](https://scholar.google.com/scholar?q=Liangming+Pan+et+al%2E+%E2%80%9CAutomatically+correcting+large+language+models%3A+Surveying+the+landscape+of+diverse+self%2Dcorrection+strategies%E2%80%9D%2E+In%3A+arXiv+preprint+arXiv%3A2308%2E03188+%282023%29%2E)
50. Hammond Pearce et al. “Asleep at the Keyboard? Assessing the Security of GitHub Copilot’s Code Contributions”. In: 43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022. IEEE, 2022, pp. 754–768. doi: 10.1109/SP46214.2022.9833571. url: https://doi.org/10.1109/S… — [doi:10.1109/sp46214.2022.9833571](https://doi.org/10.1109/sp46214.2022.9833571) [find](https://scholar.google.com/scholar?q=Hammond+Pearce+et+al%2E+%E2%80%9CAsleep+at+the+Keyboard%3F+Assessing+the+Security+of+GitHub+Copilot%E2%80%99s+Code+Contributions%E2%80%9D%2E+In%3A+43rd+IEEE+Symposium+on+Security+and+Privacy%2C+SP+2022%2C+San+Francisco%2C+CA%2C+USA%2C+May+22%2D)
51. Kexin Pei et al. “Can Large Language Models Reason about Program Invariants?” In: International Conference on Machine Learning, ICML 2023, 23-29 July 2023, Honolulu, Hawaii, USA. Ed. by Andreas Krause et al. Vol. 202. Proceedings of Machine Learning Research. PMLR, 2023, pp. 27496–27520. url: https:… [find](https://scholar.google.com/scholar?q=Kexin+Pei+et+al%2E+%E2%80%9CCan+Large+Language+Models+Reason+about+Program+Invariants%3F%E2%80%9D+In%3A+International+Conference+on+Machine+Learning%2C+ICML+2023%2C+23%2D29+July+2023%2C+Honolulu%2C+Hawaii%2C+USA%2E+Ed%2E+by+Andreas+Krause)
52. Neil Perry et al. “Do Users Write More Insecure Code with AI Assistants?” In: CoRR abs/2211.03622 (2022). doi: 10 . 48550 / arXiv . 2211 . 03622. Clover: Closed-Loop Verifiable Code Generation arXiv: 2211 . 03622. url: https://doi.org/10 . 48550 / arXiv. 2211 . 03622. — [arXiv:2211.03622](https://arxiv.org/abs/2211.03622) [find](https://scholar.google.com/scholar?q=Neil+Perry+et+al%2E+%E2%80%9CDo+Users+Write+More+Insecure+Code+with+AI+Assistants%3F%E2%80%9D+In%3A+CoRR+abs%2F2211%2E03622+%282022%29%2E+doi%3A+10+%2E+48550+%2F+arXiv+%2E+2211+%2E+03622%2E+Clover%3A+Closed%2DLoop+Verifiable+Code+Generation+arXiv%3A+)
53. Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. “Program synthesis from polymorphic refinement types”. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016. Ed. by Chandra Krintz and Emery D… [find](https://scholar.google.com/scholar?q=Nadia+Polikarpova%2C+Ivan+Kuraj%2C+and+Armando+Solar%2DLezama%2E+%E2%80%9CProgram+synthesis+from+polymorphic+refinement+types%E2%80%9D%2E+In%3A+Proceedings+of+the+37th+ACM+SIGPLAN+Conference+on+Programming+Language+Design+and+Im)
54. Gabriel Ryan et al. “Code-Aware Prompting: A study of Coverage Guided Test Generation in Regression Setting using LLM”. In: arXiv preprint arXiv:2402.00097 (2024). — [arXiv:2402.00097](https://arxiv.org/abs/2402.00097) [find](https://scholar.google.com/scholar?q=Gabriel+Ryan+et+al%2E+%E2%80%9CCode%2DAware+Prompting%3A+A+study+of+Coverage+Guided+Test+Generation+in+Regression+Setting+using+LLM%E2%80%9D%2E+In%3A+arXiv+preprint+arXiv%3A2402%2E00097+%282024%29%2E+%E2%80%94+%5BarXiv%3A2402%2E00097%5D%28https%3A%2F%2Farxiv%2Eo)
55. Gustavo Sandoval et al. “Lost at C: A User Study on the Security Implications of Large Language Model Code Assistants”. In: 32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 9-11, 2023. Ed. by Joseph A. Calandrino and Carmela Troncoso. USENIX Association, 2023. url: http… [find](https://scholar.google.com/scholar?q=Gustavo+Sandoval+et+al%2E+%E2%80%9CLost+at+C%3A+A+User+Study+on+the+Security+Implications+of+Large+Language+Model+Code+Assistants%E2%80%9D%2E+In%3A+32nd+USENIX+Security+Symposium%2C+USENIX+Security+2023%2C+Anaheim%2C+CA%2C+USA%2C+Augu)
56. William Saunders et al. “[Self-critiquing models for assisting human evaluators](https://md.research.elamur.ai/free/en/papers/saunders-2022-self-critiquing-models-assisting-human/)”. In: arXiv preprint arXiv:2206.05802 (2022).
57. Freda Shi et al. “[Natural Language to Code Translation with Execution](https://md.research.elamur.ai/free/en/papers/shi-2022-natural-language-code-translation-execution/)”. In: Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, EMNLP 2022, Abu Dhabi, United Arab Emirates, December 7-11, 2022. Ed. by Yoav Goldberg, Zornitsa Kozareva, and Yue Zhang. Association fo…
58. Kensen Shi et al. “CrossBeam: Learning to Search in Bottom-Up Program Synthesis”. In: The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. url: [https://openreview.net/forum?id=qhC8mr2LEKq](https://openreview.net/forum?id=qhC8mr2LEKq). [↗](https://openreview.net/forum?id=qhC8mr2LEKq)
59. Armando Solar-Lezama. [Program synthesis by sketching](https://md.research.elamur.ai/free/en/papers/lezama-2008-program-synthesis-sketching/). University of California, Berkeley, 2008.
60. Chuyue Sun, Christopher Hahn, and Caroline Trippel. “Towards Improving Verification Productivity with Circuit-Aware Translation of Natural Language to SystemVerilog Assertions”. In: First International Workshop on Deep Learning-aided Verification. 2023. [find](https://scholar.google.com/scholar?q=Chuyue+Sun%2C+Christopher+Hahn%2C+and+Caroline+Trippel%2E+%E2%80%9CTowards+Improving+Verification+Productivity+with+Circuit%2DAware+Translation+of+Natural+Language+to+SystemVerilog+Assertions%E2%80%9D%2E+In%3A+First+Internationa)
61. Chuyue Sun et al. “[Clover: Closed-Loop Verifiable Code Generation](https://md.research.elamur.ai/free/en/papers/sun-2024-clover-closed-loop-verifiable-code/)”. Version v2. In: (2024). arXiv: 2310.17807v2 [cs.AI]. — [arXiv:2310.17807](https://arxiv.org/abs/2310.17807)
62. Maxim Tabachnyk and Stoyan Nikolov. ML-Enhanced Code Completion Improves Developer Productivity. Blog. Accessed: 2022-07-26. 2022. url: [https://blog.research](https://blog.research) . google / 2022 / 07 / ml - enhanced - code - completion-improves.html. [↗](https://blog.research)
63. Abhishek Udupa et al. “TRANSIT: specifying protocols with concolic snippets”. In: ACM SIGPLAN Conference on Programming Language Design Chuyue Sun, Ying Sheng, Oded Padon, Clark Barrett and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013. Ed. by Hans-Juergen Boehm and Cormac Flanagan. A… [find](https://scholar.google.com/scholar?q=Abhishek+Udupa+et+al%2E+%E2%80%9CTRANSIT%3A+specifying+protocols+with+concolic+snippets%E2%80%9D%2E+In%3A+ACM+SIGPLAN+Conference+on+Programming+Language+Design+Chuyue+Sun%2C+Ying+Sheng%2C+Oded+Padon%2C+Clark+Barrett+and+Implementa)
64. Priyan Vaithilingam, Tianyi Zhang, and Elena L. Glassman. “Expectation vs. Experience: Evaluating the Usability of Code Generation Tools Powered by Large Language Models”. In: CHI ’22: CHI Conference on Human Factors in Computing Systems, New Orleans, LA, USA, 29 April 2022 - 5 May 2022, Extended Ab… — [doi:10.1145/3491101.3519665](https://doi.org/10.1145/3491101.3519665) [find](https://scholar.google.com/scholar?q=Priyan+Vaithilingam%2C+Tianyi+Zhang%2C+and+Elena+L%2E+Glassman%2E+%E2%80%9CExpectation+vs%2E+Experience%3A+Evaluating+the+Usability+of+Code+Generation+Tools+Powered+by+Large+Language+Models%E2%80%9D%2E+In%3A+CHI+%E2%80%9922%3A+CHI+Conference+)
65. Richard J Waldinger and Richard CT Lee. “PROW: A step toward automatic program writing”. In: Proceedings of the 1st international joint conference on Artificial intelligence. 1969, pp. 241–252. [find](https://scholar.google.com/scholar?q=Richard+J+Waldinger+and+Richard+CT+Lee%2E+%E2%80%9CPROW%3A+A+step+toward+automatic+program+writing%E2%80%9D%2E+In%3A+Proceedings+of+the+1st+international+joint+conference+on+Artificial+intelligence%2E+1969%2C+pp%2E+241%E2%80%93252%2E)
66. Xuezhi Wang et al. “[Self-consistency improves chain of thought reasoning in language models](https://md.research.elamur.ai/free/en/papers/wang-2022-self-consistency-improves-chain-thought/)”. In: arXiv preprint arXiv:2203.11171 (2022).
67. Jason Wei et al. “[Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://md.research.elamur.ai/free/en/papers/wei-2022-chain-thought-prompting-elicits-reasoning/)”. In: NeurIPS. 2022. url: [http://papers.nips.cc/paper%5C_files/paper/2022/hash/9d5609613524ecf4f15af0f7b31abca4-Abstract-Conference.html](http://papers.nips.cc/paper%5C_files/paper/2022/hash/9d5609613524ecf4f15af0f7b31abca4-Abstract-Conference.html). [↗](http://papers.nips.cc/paper%5C_files/paper/2022/hash/9d5609613524ecf4f15af0f7b31abca4-Abstract-Conference.html)
68. Cheng Wen et al. “Enchanting program specification synthesis by large language models using static analysis and program verification”. In: arXiv preprint arXiv:2404.00762 (2024). — [arXiv:2404.00762](https://arxiv.org/abs/2404.00762) [find](https://scholar.google.com/scholar?q=Cheng+Wen+et+al%2E+%E2%80%9CEnchanting+program+specification+synthesis+by+large+language+models+using+static+analysis+and+program+verification%E2%80%9D%2E+In%3A+arXiv+preprint+arXiv%3A2404%2E00762+%282024%29%2E+%E2%80%94+%5BarXiv%3A2404%2E00762%5D%28)
69. Haoze Wu, Clark Barrett, and Nina Narodytska. [Lemur: Integrating Large Language Models in Automated Program Verification](https://md.research.elamur.ai/free/en/papers/wu-2024-lemur-integrating-large-language-models/). 2023. arXiv: 2310. 04870 [cs.FL].
70. Frank F. Xu, Bogdan Vasilescu, and Graham Neubig. “In-IDE Code Generation from Natural Language: Promise and Challenges”. In: ACM Trans. Softw. Eng. Methodol. 31.2 (2022), 29:1–29:47. doi: 10 . 1145 / 3487569. url: https://doi.org/10.1145/3487569. [↗](https://doi.org/10.1145/3487569)
71. Pengcheng Yin and Graham Neubig. “[A Syntactic Neural Model for General-Purpose Code Generation](https://md.research.elamur.ai/free/en/papers/yin-2017-syntactic-neural-model-general-purpose/)”. In: Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics, ACL 2017, Vancouver, Canada, July 30 - August 4, Volume 1: Long Papers. Ed. by Regina Barzilay and Min-Yen Kan…
72. Pengcheng Yin et al. “[Natural Language to Code Generation in Interactive Data Science Notebooks](https://md.research.elamur.ai/free/en/papers/yin-2023-natural-language-code-generation-interactive/)”. In: Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2023, Toronto, Canada, July 9-14, 2023. Ed. by Anna Rogers, Jordan L. Boyd-Graber…
73. Eric Zelikman et al. “Parsel: A (de-) compositional framework for algorithmic reasoning with language models”. In: arXiv preprint arXiv:2212.[10561 (2023)](https://md.research.elamur.ai/free/en/papers/zelikman-2023-parsel-algorithmic-reasoning-language-models/).
74. Tianyi Zhang et al. “[Coder Reviewer Reranking for Code Generation](https://md.research.elamur.ai/free/en/papers/zhang-2022-coder-reviewer-reranking-code-generation/)”. In: International Conference on Machine Learning, ICML 2023, 23-29 July 2023, Honolulu, Hawaii, USA. Ed. by Andreas Krause et al. Vol. 202. Proceedings of Machine Learning Research. PMLR, 2023, pp. 41832–41846. url: https://proceedi…
75. Baishun Zhou and Gangyi Ding. “Survey of intelligent program synthesis techniques”. In: International Conference on Algorithms, High Performance Computing, and Artificial Intelligence (AHPCAI 2023). Ed. by Sandeep Saxena and Cairong Zhao. Vol. 12941. International Society for Optics and Photonics. S… — [doi:10.1117/12.3011627](https://doi.org/10.1117/12.3011627) [find](https://scholar.google.com/scholar?q=Baishun+Zhou+and+Gangyi+Ding%2E+%E2%80%9CSurvey+of+intelligent+program+synthesis+techniques%E2%80%9D%2E+In%3A+International+Conference+on+Algorithms%2C+High+Performance+Computing%2C+and+Artificial+Intelligence+%28AHPCAI+2023%29%2E+E)

*Updated 3 November 2026*