Content area
Abstract
The last few years have seen much progress in two related but traditionally disjoint areas of research: program repair and program synthesis. Program repair is the problem of locating and removing faults in a given faulty program. Program synthesis is the problem of generating programs automatically from high-level specifications. While innovation in each of these two research areas has been impressive, the techniques developed within one area have largely been confined to that area. Our insight is that the unification of program repair and program synthesis holds a key to developing well-founded, systematic, and scalable tools for repairing complex defects. The contribution of this dissertation is three-fold: a synthesis-based approach SketchRep for program repair based on propositional satisfiability solving, an execution-driven synthesis engine EdSketch for Java, and a program repair approach SketchFix to repair defects at the AST node-level with execution-driven sketching.
SketchRep is a debugging approach that reduces the problem of program repair to a sub-problem of program synthesis, namely program sketching, in which the user writes a sketch, i.e., an incomplete program that has holes, and automated tools complete the sketch with respect to the given specification or reference implementation. Our program repair approach translates the given faulty program to a sketch and leverages an off-the-shelf inductive synthesizer to fill in the holes of the incomplete program with respect to the given test suite.
EdSketch is an execution-driven synthesis engine for Java. Traditional solutions to the sketching problem perform a translation to SAT formulas. While effective for a range of programs, when applied to real applications, such translation-based approaches may lead to impractical problems to trans- late all relevant libraries to SAT. Instead of transforming the program to logic formulas for SAT solvers, EdSketch explores the actual program behaviors in presence of libraries and provides a practical solution to sketching small parts of real-world applications.
SketchFix is a repair technique that generates candidate fixes on demand during the test execution. It translates faulty programs to sketches, compiles each sketch once which may represent a large number of concrete candidates, and lazily initializes the candidates of the sketches while validating them against the test execution.
The dissertation describes each technique and presents experimental results that demonstrate its efficacy.