Much effort is spent by programmers everyday in trying to reduce long, failing execution traces to the cause of the error. We present an algorithm for error cause localization based on a reduction to the maximal satisï¬�ability problem (MAX-SAT), which asks what is the maximum number of clauses of a Boolean formula that can be simultaneously satisï¬�ed by an assignment. At an intuitive level, our algorithm takes as input a program and a failing test, and comprises the following three steps. First, using bounded model checking, and a bound obtained from the execution of the test, we encode the semantics of a bounded unrolling of the program as a Boolean trace formula. Second, for a failing program execution (e.g., one that violates an assertion or a post-condition), we construct an unsatisï¬�able formula by taking the formula and additionally asserting that the input is the failing test and that the assertion condition does hold at the end. Third, using MAX-SAT, we ï¬�nd a maximal set of clauses in this formula that can be satisï¬�ed together, and output the complement set as a potential cause of the error.

 

We have implemented our algorithm in a tool called BugAssist that performs error localization for C programs. We demonstrate the effectiveness of BugAssist on a set of benchmark examples with injected faults, and show that in most cases, BugAssist can quickly and precisely isolate a few lines of code whose change eliminates the error. We also demonstrate how our algorithm can be modiï¬�ed to automatically suggest ï¬�xes for common classes of errors such as off-by-one.