Counterexamples Revisited: Principles, Algorithms, Applications

Algorithmic counterexample generation is a central feature of model checking which sets the method apart from other approaches such as theorem proving. The practical value of counterexamples to the verification engineer is evident, and for many years, counterexample generation algorithms have been employed in model checking systems, even though they had not been subject to an adequate fundamental investigation. Recent advances in model checking technology such as counterexample-guided abstraction refinement have put strong emphasis on counterexamples, and have lead to renewed interest both in fundamental and pragmatic aspects of counterexample generation. In this paper, we survey several key contributions to the subject including symbolic algorithms, results about the graph-theoretic structure of counterexamples, and applications to automated abstraction as well as software verification.Irrefutability is not a virtue of a theory (as people often think) but a vice. Karl R. Popper