HackerPapers

arXiv:2209.01766cs.SE

Exploring the Verifiability of Code Generated by GitHub Copilot

Dakota Wong, Austin Kothig, Patrick Lam

HN submission. Found in a submission link or body. Submitters do not count as commenters in the main ranking; a submission is not an endorsement.

Abstract

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.

arXiv comments
HATRA workshop at SPLASH 2022
Journal reference
DOI
Subjects
cs.SESoftware Engineering cs.PLProgramming Languages

On Hacker News

No comments linking this paper were found in the collected sources. Found in 1 HN submission from Mar 2024 to Mar 2024. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments0 threads

No comments linking this paper were found in the collected sources. Open submission discussions.

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.