Paper Info
Title
Sound and Complete Mutation-Based Program Repair.
Abstract
This work presents a novel approach for automatically repairing an erroneous program with respect to a given set of assertions. Programs are repaired using a predefined set of mutations. We refer to a bounded notion of correctness, even though, for a large enough bound all returned programs are fully correct. To ensure no changes are made to the original program unless necessary, if a program can be repaired by applying a set of mutations Mut, then no superset of Mut is later considered. Programs are checked in increasing number of mutations, and every minimal repaired program is returned as soon as found. We impose no assumptions on the number of erroneous locations in the program, yet we are able to guarantee soundness and completeness. That is, we assure that a program is returned iff it is minimal and bounded correct. Searching the space of mutated programs is reduced to searching unsatisfiable sets of constraints, which is performed efficiently using a sophisticated cooperation between SAT and SMT solvers. Similarities between mutated programs are exploited in a new way, by using both the SAT and the SMT solvers incrementally. We implemented a prototype of our algorithm, compared it with a state-of-the-art repair tool and got very encouraging results.
Year
DOI
Venue
2016
10.1007/978-3-319-48989-6_36
Lecture Notes in Computer Science
Field
DocType
Volume
Subset and superset,Computer science,Correctness,Theoretical computer science,Bounded function
Conference
9995
ISSN
Citations 
PageRank 
0302-9743
4
0.53
References 
Authors
19
2
Name
Order
Citations
PageRank
Bat-Chen Rothenberg181.60
Orna Grumberg24361351.99