Exploring the Verifiability of Code Generated by GitHub Copilot
Not on the map. Why?
Abstract (arXiv)
GitHub's Copilot generates code quickly. We investigate whether it generates good code. Our approach is to identify a set of problems, ask Copilot to generate solutions, and attempt to formally verify these solutions with Dafny. Our formal verification is with respect to hand-crafted specifications. We have carried out this process on 6 problems and succeeded in formally verifying 4 of the created solutions. We found evidence which corroborates the current consensus in the literature: Copilot is a powerful tool; however, it should not be "flying the plane" by itself.
Key facts. Cited by 4 papers in the map (data through 7 Oct 2026). First posted on arXiv 5 Sep 2022.
Builds on
No reference list yet.
Built on by
Citing papers per year: 2023: 3; 2024: 1.
4 papers.
- 2024Bugs in Large Language Models Generated Code: An Empirical Studycited by 59
- 2023Is AI the better programming partner? Human-Human Pair Programming vs. Human-AI pAIr Programmingcited by 20
- 2023Turbulence: Systematically and Automatically Testing Instruction-Tuned Large Language Models for Codecited by 9
- 2023Numeracy from Literacy: Data Science as an Emergent Skill from Large Language Modelscited by 8
- 2024Bugs in Large Language Models Generated Code: An Empirical Study13 Mar 2024
- 2023Turbulence: Systematically and Automatically Testing Instruction-Tuned Large Language Models for Code22 Dec 2023
- 2023Is AI the better programming partner? Human-Human Pair Programming vs. Human-AI pAIr Programming8 Jun 2023
- 2023Numeracy from Literacy: Data Science as an Emergent Skill from Large Language Models31 Jan 2023