The Taub Faculty of Computer Science Events and Talks

This work presents a novel approach for automatically repairing a program with respect to a given set of assertions. Programs are repaired using a predefined set of mutations. 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 every returned program is correct and every correct program is returned. We refer to a bounded notion of correctness, even though, due to completeness, any unbounded correct program will be found, if exists. The repaired programs are returned one by one, in increasing number of mutations. Only minimal sets of mutations are applied. That is, if a program can be repaired by applying a set of mutations Mut, then no superset of Mut is later considered. This is based on the understanding that the programmer would like to get a repaired program that is as close to the original program as possible. Our approach is entirely based on formal methods, avoiding any use of testing. Specifically, we exploit both SMT and SAT solvers, both incrementally. The SMT solver verifies whether a mutated program is indeed correct. The SAT solver restricts the search space of mutated programs to only those obtained by a minimal mutation set. Thus, an eficient search of all minimal repaired program is achieved. We implemented a prototype of our algorithm and got very encouraging results.