# Verifix: Verified Repair of Programming Assignments

arXiv: https://arxiv.org/abs/2106.16199 · HTML: https://mlsanity.com/paper/2106.16199/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Jun 2021.

## Built on by (most cited first, 7 of 7)

- [Repairing Bugs in Python Assignments Using Large Language Models](https://mlsanity.com/paper/2209.14876/) (2022)
- [Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization](https://mlsanity.com/paper/2502.07786/) (2024)
- [C-Pack of IPAs: A C90 Program Benchmark of Introductory Programming Assignments](https://mlsanity.com/paper/2206.08768/) (2022)
- [InvAASTCluster: On Applying Invariant-Based Program Clustering to Introductory Programming Assignments](https://mlsanity.com/paper/2206.14175/) (2022)
- [VeriPilot: An LLM-Powered Verilog Debugging Framework](https://mlsanity.com/paper/2606.23759/) (2026)
- [Graph Neural Networks For Mapping Variables Between Programs -- Extended Version](https://mlsanity.com/paper/2307.13014/) (2023)
- [Peer-aided Repairer: Empowering Large Language Models to Repair Advanced Student Assignments](https://mlsanity.com/paper/2404.01754/) (2024)

## Abstract (arXiv)

Automated feedback generation for introductory programming assignments is useful for programming education. Most works try to generate feedback to correct a student program by comparing its behavior with an instructor's reference program on selected tests. In this work, our aim is to generate verifiably correct program repairs as student feedback. The student assignment is aligned and composed with a reference solution in terms of control flow, and differences in data variables are automatically summarized via predicates to relate the variable names. Failed verification attempts for the equivalence of the two programs are exploited to obtain a collection of maxSMT queries, whose solutions point to repairs of the student assignment. We have conducted experiments on student assignments curated from a widely deployed intelligent tutoring system. Our results indicate that we can generate verified feedback in up to 58% of the assignments. More importantly, our system indicates when it is able to generate a verified feedback, which is then usable by novice students with high confidence.