论文标题
探索GitHub Copilot生成的代码的可验证性
Exploring the Verifiability of Code Generated by GitHub Copilot
论文作者
论文摘要
Github的副驾驶员快速生成代码。我们研究它是否生成良好的代码。我们的方法是确定一组问题，要求Copilot生成解决方案，并尝试使用DAFNY正式验证这些解决方案。我们的正式验证是关于手工制作的规格。我们已经在6个问题上进行了此过程，并成功地正式验证了创建解决方案的4个。我们找到了证实文献中当前共识的证据：副驾驶是一种强大的工具；但是，它本身不应“飞行”。
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.
