探索GitHub Copilot生成代码的可验证性
软件工程
2022-10-28 v2 编程语言
摘要
GitHub的Copilot可快速生成代码。我们研究其是否生成优质代码。我们的方法是确定一组问题，让Copilot生成解决方案，并尝试用Dafny对这些方案进行形式化验证。我们的形式化验证基于手工编写的规约。我们已对6个问题执行该过程，并成功形式化验证了其中4个所创建的方案。我们发现的证据印证了文献中的当前共识：Copilot是一款强大工具；然而，它不应独自“驾驶飞机”。
关键词
引用
@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}
}
备注
HATRA workshop at SPLASH 2022