Repair of Boolean Programs using Games

Andreas Griesmayer and Roderick Bloem

Graz University of Technology


We show how to find and fix faults in Boolean programs by extending the program to a game. In the game, the protagonist can choose which statement is incorrect and how to repair it. If she can do this successfully using a memoryless strategy, we have found a fault plus a correction. We discuss how this technique can be used to fix faults in programs written in a language like C, by using the Boolean programs that are produced as abstractions in approaches such as SLAM and MAGIC. Last updated: May 23, 2005