Repair of Boolean Programs with an Application to C

We show how to find and fix faults in Boolean programs by extending the program to a game. In the game, the protagonist can select an alternative implementation for an incorrect statement. If the protagonist can do so successfully using a memoryless strategy that does not depend on the stack contents, we have found a correction for the Boolean program. We present a symbolic algorithm that localizes possibly faulty statements and provides corrections. oolean program is an abstraction of a C program, the repair for the Boolean program suggests a repair for the original C program. This yields a correct but incomplete approach to repairing C programs. We have applied this apo Boolean programs that are produced as abstractions by SLAM and have thus successfully patched several faulty Windows device drivers.

• Type: Conference
• Year: 2006
• Where: CAV
• Authors: Andreas Griesmayer, Roderick Bloem, Byron Cook
• Keywords: Apo Boolean Programs, Boolean Programs, CAV 2006, Hardware, Incorrect Statement