  Fault localization is a practical research topic that helps developers
identify code locations that might cause bugs in a program. Most existing fault
localization techniques are designed for imperative programs (e.g., C and Java)
and rely on analyzing correct and incorrect executions of the program to
identify suspicious statements. In this work, we introduce a fault localization
approach for models written in a declarative language, where the models are not
"executed," but rather converted into a logical formula and solved using
backend constraint solvers. We present FLACK, a tool that takes as input an
Alloy model consisting of some violated assertion and returns a ranked list of
suspicious expressions contributing to the assertion violation. The key idea is
to analyze the differences between counterexamples, i.e., instances of the
model that do not satisfy the assertion, and instances that do satisfy the
assertion to find suspicious expressions in the input model. The experimental
results show that FLACK is efficient (can handle complex, real-world Alloy
models with thousand lines of code within 5 seconds), accurate (can
consistently rank buggy expressions in the top 1.9\% of the suspicious list),
and useful (can often narrow down the error to the exact location within the
suspicious expressions).
