Path-Based Program Repair

TL;DR

This paper introduces a path-based program repair method for imperative programs that iteratively refines repairs using symbolic counterexamples, directly deriving fixes from logic specifications, and is complete for programs with finite control-flow paths.

Contribution

The paper presents a novel, complete path-based repair framework that efficiently repairs programs by combining symbolic data-flow analysis with control-flow considerations.

Findings

Approach is effective for small programs.

Repairs are directly derived from logic specifications.

Method is complete for programs with finitely many control-flow paths.

Abstract

We propose a path-based approach to program repair for imperative programs. Our repair framework takes as input a faulty program, a logic specification that is refuted, and a hint where the fault may be located. An iterative abstraction refinement loop is then used to repair the program: in each iteration, the faulty program part is re-synthesized considering a symbolic counterexample, where the control-flow is kept concrete but the data-flow is symbolic. The appeal of the idea is two-fold: 1) the approach lazily considers candidate repairs and 2) the repairs are directly derived from the logic specification. In contrast to prior work, our approach is complete for programs with finitely many control-flow paths, i.e., the program is repaired if and only if it can be repaired at the specified fault location. Initial results for small programs indicate that the approach is useful for debugging programs in practice.