Exploring the Verifiability of Code Generated by GitHub Copilot
summary
Authors feed six algorithmic problems to GitHub Copilot, add hand‑crafted pre/postconditions and loop invariants, translate generated Python into Dafny, and attempt formal proofs. Four of six solutions verify; binary search and two‑sum verify after writing predicates, variants and seven invariants for nested loops. Prime‑factors times out during proof attempts and requires extra library lemmas; the max‑subarray solution is O(n^2), resists a correctness proof and cannot be discharged automatically.
AI-written summary · about
chapters (13)
- 0:00Verifying Copilot-generated code
- 1:05What GitHub Copilot does
- 2:35Prior research on correctness
- 7:58Verifying Copilot's Python code
- 9:03Problem selection approach
- 12:19Binary search verification
- 14:27Two sums verification
- 15:34Prime factors failure case
- 17:41Max heap issues
- 19:25Course project context
- 20:07Key findings
- 21:30Challenges and future work
- 22:31Q&A
related talks
49mUnlocking Success: Navigating the Code of Life with GitHub CoPilot
24mGitHub Copilot Agents + Sonar | The Blueprint for Agentic Development
57mUnlocking Success: Navigating the Code of Life with GitHub CoPilot
20mCLOVER: Closed-Loop Verifiable Code Generation
31mSolving AdventOfCode with GitHub Copilot and OpenAI ChatGTP
31mGithub Co-Pilot: Addictive or Effective?
40mUnlocking Productivity with GitHub Copilot Best Practices and Tips
16mShift Left with GitHub Copilot: Enforcing Code Quality Before the Commit