Execution-free Program Repair
Li Huang, Bertrand Meyer, Ilgiz Mustafin, Manuel Oriol
TL;DR
The paper presents Proof-2-Fix, a static, prover-based automatic program repair approach that replaces dynamic test-driven repair with formal verification. When verification fails, it uses counterexamples to infer invariants with Daikon, then synthesizes candidate fixes that are validated by the prover, yielding contract or implementation changes. Evaluation on Eiffel programs shows high success rates, with fixes verified by proof and reasonable runtime, highlighting advantages in correctness guarantees and reduced reliance on test suites. The work outlines plans to broaden invariant power, fix schemas, and IDE integration, aiming to make automatic repair a routine part of software development.
Abstract
Automatic program repair usually relies heavily on test cases for both bug identification and fix validation. The issue is that writing test cases is tedious, running them takes much time, and validating a fix through tests does not guarantee its correctness. The novel idea in the Proof2Fix methodology and tool presented here is to rely instead on a program prover, without the need to run tests or to run the program at all. Results show that Proof2Fix finds and fixes significant historical bugs.