Fault Localization in Multi-Threaded C Programs using Bounded Model Checking (extended version)

Abstract

—Software debugging is a very time-consuming process, which is even worse for multi-threaded programs, due to the non-deterministic behavior of thread-scheduling algorithms. However, the debugging time may be greatly reduced, if automatic methods are used for localizing faults. In this study, a new method for fault localization, in multi-threaded C programs, is proposed. It transforms a multi-threaded program into a correspondin g sequential one and then uses a fault-diagnosis method suitable for this type of program, in order to localize faults. The cod e transformation is implemented with rules and context switc h information from counterexamples, which are typically generated by bounded model checkers. Experimental results show that the proposed method is effective, in such a way that sequential faultlocalization methods can be extended to multi-threaded programs.