Exploring the Verifiability of Code Generated by GitHub Copilot

Dakota Wong; Austin Kothig; Patrick Lam

Exploring the Verifiability of Code Generated by GitHub Copilot

Software Engineering 2022-10-28 v2 Programming Languages

Authors: Dakota Wong , Austin Kothig , Patrick Lam

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.

Keywords

software refactoring code generation

Cite

@article{arxiv.2209.01766,
  title  = {Exploring the Verifiability of Code Generated by GitHub Copilot},
  author = {Dakota Wong and Austin Kothig and Patrick Lam},
  journal= {arXiv preprint arXiv:2209.01766},
  year   = {2022}
}

Comments

HATRA workshop at SPLASH 2022

Related papers

View all related →