GitHub Copilot生成代码的可验证性研究
Exploring the Verifiability of Code Generated by GitHub Copilot
摘要：
GitHub的Copilot可以快速生成代码。我们研究它是否生成好的代码。我们的方法是识别一组问题，要求Copilot生成解决方案，并尝试与Dafny正式验证这些解决方案。我们的形式化验证是关于手工制作的规范。我们已经对6个问题进行了这个过程，并成功地正式验证了其中4个创建的解决方案。我们发现的证据证实了文献中目前的共识：Copilot是一个强大的工具;然而，它不应该自己“驾驶飞机”。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
