Towards Automated Verification of LLM-Synthesized C Programs

This conference talk from CoqPL 2025 presents SYNVER, a novel synthesis and verification framework for C programs that leverages Large Language Models (LLMs) to generate candidate programs satisfying given specifications. Explore how researchers Prasita Mukherjee and Benjamin Delaware impose biases on specifications and programs to make LLM-synthesized code more amenable to automated verification. Learn about their innovative specification-verification tool built on top of Verified Software Toolchain that helps automate the verification process. The 22-minute presentation was delivered at the CoqPL 2025 workshop on January 25, 2025, sponsored by ACM SIGPLAN.