Finding and fixing faults (Q414907)

The promises of fault localization and correction for finite state systems sound like magic. However, the algorithm proposed by the authors makes intuitive sense, and it is given a reasonably clear exposition in the paper. The algorithm extracts a ``correction'' from a winning strategy for a game, constructed from the original program and its specification (expressed in linear temporal logic). The authors apply their algorithm to six examples: unfortunately, all six examples are small in scope and tersely presented. It remains unclear whether larger examples remain tractable with this level of automation.