Verifix: Verified Repair of Programming Assignments

TL;DR

Verifix automatically generates verifiably correct program repairs as feedback for student assignments by aligning student and reference programs, analyzing differences, and using maxSMT queries, achieving up to 58% success.

Contribution

This work introduces a novel approach to generate verified program repairs for student feedback using program alignment, predicate summarization, and maxSMT solving, with experimental validation.

Findings

Achieved verified feedback generation for up to 58% of assignments.

System confidently indicates when verified feedback can be generated.

Effective in real-world educational settings with student assignments.

Abstract

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.