Batchen Rothenberg, M.Sc. Thesis Seminar
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