Program repair as a game

B Jobstmann, A Griesmayer, R Bloem - … Edinburgh, Scotland, UK, July 6-10 …, 2005 - Springer
Computer Aided Verification: 17th International Conference, CAV 2005 …, 2005Springer
We present a conservative method to automatically fix faults in a finite state program by
considering the repair problem as a game. The game consists of the product of a modified
version of the program and an automaton representing the LTL specification. Every winning
finite state strategy for the game corresponds to a repair. The opposite does not hold, but we
show conditions under which the existence of a winning strategy is guaranteed. A finite state
strategy corresponds to a repair that adds variables to the program, which we argue is …
Abstract
We present a conservative method to automatically fix faults in a finite state program by considering the repair problem as a game. The game consists of the product of a modified version of the program and an automaton representing the LTL specification. Every winning finite state strategy for the game corresponds to a repair. The opposite does not hold, but we show conditions under which the existence of a winning strategy is guaranteed. A finite state strategy corresponds to a repair that adds variables to the program, which we argue is undesirable. To avoid extra state, we need a memoryless strategy. We show that the problem of finding a memoryless strategy is NP-complete and present a heuristic. We have implemented the approach symbolically and present initial evidence of its usefulness.
Springer