Automated Error Localization with Weighted Partial Maximum Satisfiability

摘要

Localizing error in programs is a hard task that requires human engineers to find real bug locations with the manual analysis of lengthy counterexample traces. Automatic error localization methods exist but they often generate many spurious root causes. This paper proposes a new method for localizing error in imperative programs. It uses weighted partial Maximum Satisfiability (MaxSAT) and several advanced techniques. The proposed method is implemented in SNIPER, a tool build upon the LLVM compiler infrastructure and the Yices SMT solver. We demonstrate the effectiveness of SNIPER on the TCAS task of the Siemens Test Suite.