Stryker: Scaling Specification-Based Program Repair by Pruning Infeasible Mutants with SAT

TL;DR

Stryker introduces a SAT-based pruning technique to efficiently explore and repair multiple bugs in Java programs by considering extensive intra-statement transformations and eliminating infeasible fix candidates.

Contribution

The paper presents a novel pruning mechanism in program repair that enables exhaustive intra-statement fix exploration while efficiently eliminating infeasible candidates.

Findings

Successfully repaired multi-bug Java programs

Pruned large candidate spaces effectively

Enabled exhaustive intra-statement modifications

Abstract

Many techniques for automated program repair involve syntactic program transformations. Applying combinations of such transformations on faulty code yields fix candidates whose correctness must be determined. Exploring these combinations leads to an explosion on the number of generated fix candidates that severely limits the applicability of such fault repair techniques. This explosion is most times tamed by not considering fix candidates exhaustively, and by disabling intra-statement modifications. In this article we present a technique for program repair that considers an ample set of intra-statement syntactic operations, and explores fix candidates exhaustively up to a provided bound. The suitability of the technique, implemented in our tool Stryker, is supported by a novel mechanism to detect and prune infeasible fix candidates. This allows Stryker to repair programs with several bugs, whose fixes require multiple modifications. We evaluate our technique on a benchmark of faulty Java container classes, which Stryker is able to repair, pruning significant parts of the space of generated candidates when more than one bug is present in the code.