Abstract If a program does not fulfill its specification, a model checker can deliver a counterexample. However, although such a counterexample shows how the specification can be violated, it typically comprises large parts of the program and gives little information about which of the visited statements is responsible for the error. In this article, we show that model checkers can also be used to perform model‐based diagnosis and thus fault localization. The approach leads to significantly more precise diagnoses than the state‐of‐the‐art and typically rules out 90–99% of the code as possible fault locations. The approach is general and can be applied to any system that is amenable to model checking (with respect to language and complexity). To demonstrate the applicability and high precision of our approach, we present implementations for C programs using two different model checking tools and show experimental results from the TCAS case study and an integration with the DDVerify framework to debug Linux device drivers. Copyright © 2009 John Wiley & Sons, Ltd.

We present an efficient fully automatic approach to fault localization for safety properties stated in linear temporal logic. We view the failure as a contradiction between the specification and the actual behavior and look for components that explain this discrepancy. We find these components by solving the satisfiability of a propositional Boolean formula. We show how to construct this formula and how to extend it so that we find exactly those components that can be used to repair the circuit for a given set of counterexamples. Furthermore, we discuss how to efficiently solve the formula by using the proper decision heuristics and simulation-based preprocessing. We demonstrate the quality and efficiency of our approach by experimental results.