Counterexample Guided Program Repair Using Large Language Models and MaxSAT-based Fault Localization

Debugging and repair are costly in both software development and programming education. This talk presents two approaches that combine formal methods with large language models (LLMs) to improve accuracy and scalability. First, we introduce CFaults, a MaxSAT-based fault localization tool for C programs that ensures consistent, subset-minimal diagnoses across multiple failing tests. It outperforms existing tools like BugAssist and SNIPER in speed and precision. Second, we apply a hybrid method to automated repair of C code, using MaxSAT, CFaults, to localize bugs and LLMs to replace the faulty code via a counterexample-guided loop. This approach produces more targeted and effective repairs than existing symbolic or LLM-only methods, improving outcomes across over 1,400 incorrect student submissions. Together, these methods show how combining formal reasoning with generative models enables more efficient and precise debugging and repair.

Jun 23, 2025 12:00 PM — 1:00 PM