CLOVER: Closed-Loop Verifiable Code Generation - Dafny'24
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore a groundbreaking approach to ensuring correctness in AI-generated code through this 20-minute conference talk presented at ACM SIGPLAN. Dive into the Clover (Closed-Loop Verifiable Code Generation) paradigm, which transforms correctness checking into a more manageable consistency checking problem. Learn about the innovative checker that utilizes formal verification tools and large language models to perform consistency checks among code, docstrings, and formal annotations. Examine the theoretical analysis supporting Clover's effectiveness and review empirical findings from the CloverBench dataset, featuring annotated Dafny programs. Discover how large language models show promise in automatically generating formal specifications and explore the consistency checker's impressive acceptance rate for correct instances while maintaining zero tolerance for incorrect ones.
Syllabus
[Dafny'24] CLOVER: Closed-Loop Verifiable Code Generation
Taught by
ACM SIGPLAN
Related Courses
Software as a ServiceUniversity of California, Berkeley via Coursera Software Testing
University of Utah via Udacity The Hardware/Software Interface
University of Washington via Coursera Software Debugging
Saarland University via Udacity Introduction to Systematic Program Design - Part 1
The University of British Columbia via Coursera