Automated Repair of Termination Errors

Automated program repair aims to identify a syntactic change that converts an incorrect program into one that complies with a given specification. While previous works mostly focused on repairing violations of safety properties, little attention has been paid to termination errors, despite their prevalence in practice. In this study, we introduce the first program repair approach that synthesises patches to enable programs with infinite loops to provably terminate. Repairing termination errors presents a challenge as the violation witnesses of this property are infinite traces. To address this difficulty, we formulate the repair problem as a simultaneous synthesis of a patch and a ranking function that proves the patched program terminates. We solve this problem by generating repair constraints from a modified termination proving approach based on disjunctive well-foundedness principle, and solve these constraints using counter-example guided inductive synthesis. Additionally, we propose heuristics that deprioritise trivial incorrect repairs that disable loop execution instead of repairing the bug. An evaluation on realistic termination errors extracted from open source projects demonstrated that our approach correctly repaired 8 of 19 bugs caused by infinite loops