Exploring the Verifiability of Copilot

Introduction:

• This paper along with its additional works explore the verifiability of Copilot generated python programs using the Dafny programming language.

• The PDF version of the paper is named paper.pdf. The verified programs from the paper and some additional works can be found in the copilot_verification folder.

• Presented at SPLASH 2022 during the Human Aspects of Types and Reasoning Assistants (HATRA) Workshop

Contributers:

• Dakota Wong, University of Waterloo, Canada

• Austin Kothig, University of Waterloo, Canada

• Patrick Lam, University of Waterloo, Canada

Links:

• HATRA 2022:   https://2022.splashcon.org/details/hatra-2022-papers/4/Exploring-the-Verifiability-of-Code-Generated-by-GitHub-Copilot
• Publication:   https://arxiv.org/abs/2209.01766