Program repair as a game. (English) Zbl 1081.68572

Etessami, Kousha (ed.) et al., Computer aided verification. 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6–10, 2005. Proceedings. Berlin: Springer (ISBN 3-540-27231-3/pbk). Lecture Notes in Computer Science 3576, 226-238 (2005).
Summary: 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.
For the entire collection see [Zbl 1078.68004].


68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
91A80 Applications of game theory
Full Text: DOI