Execution-free Program Repair
Li Huang, Bertrand Meyer, Ilgiz Mustafin, Manuel Oriol

TL;DR
Proof2Fix introduces a novel approach to program repair that uses a program prover instead of test cases, enabling bug fixing without executing the program, thus addressing test-related challenges.
Contribution
This paper presents Proof2Fix, a new method that repairs programs using formal proofs rather than test execution, reducing reliance on test cases.
Findings
Proof2Fix successfully repairs historical bugs.
The approach eliminates the need for program execution during repair.
Proof2Fix demonstrates effectiveness on real-world bugs.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDistributed systems and fault tolerance · Security and Verification in Computing · Radiation Effects in Electronics
