Repair of Boolean Programs with an Application to C
Repair of Boolean Programs with an Application to C
复制标题
应用 C 语言修复布尔程序
DOI：
10.1007/11817963_33
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
B. Cook
中科院分区：
文献类型：
--
作者：
Andreas Griesmayer;R. Bloem;B. Cook
我们展示了如何通过将程序扩展到游戏来查找和修复布尔程序中的错误。在游戏中，主角可以为不正确的陈述选择一个替代实现。如果主人公可以使用不依赖于堆栈内容的无记忆策略成功地做到这一点，我们就找到了对布尔程序的修正。我们提出了一种符号算法，它可以定位可能有错误的语句并提供更正。
如果布尔程序是C程序的抽象，那么对布尔程序的修复就是对原始C程序的修复。这产生了修复C程序的正确但不完整的方法。我们已经将这种方法应用于由SLAM作为抽象生成的布尔程序，从而成功地修补了几个有缺陷的Windows设备驱动程序。
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.
If the Boolean 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 approach to Boolean programs that are produced as abstractions by SLAM and have thus successfully patched several faulty Windows device drivers.