A bounded constraint-based approach to aid in fault localization from a counterexample

A model checker can produce a trace of counter-example for an erroneous program, which is often difficult to exploit for locating faults. In this paper, we propose a fault localization algorithm from counter-examples, named LocFaults, combining the approaches of Bounded Model-Checking (BMC) with a constraint satisfaction problem (CSP). The input is a faulty program for which a counter-example and a postcondition are provided. To identify helpful information for fault location, LocFaults analyzes the paths of the CFG (Control Flow Graph) of the erroneous program to calculate the subsets of suspicious instructions to correct the program. Indeed, we generate a system of constraints for paths of the control flow graph for which at most k conditional statements can be wrong. Then we calculate the MCSs (Minimal Correction Sets) of limited size on each of these paths. The removal of one of these sets of constraints yields a maximal satisfiable subset, in other words, a maximal subset of constraints satisfying the postcondition. LocFaults has been experimentally evaluated on a set of academic and realistic programs. The main advantage of this flow-driven approach is that the computed sets of suspicious instructions are small, each of them being associated with an identified path. Moreover, the constraint programming-based framework of LocFaults allows mixing Boolean and numerical constraints in an efficient and straightforward way.