Counterexamples revisited: Principles, algorithms, applications

Abstract. 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, counterexam-ple generation algorithms have been employed in model checking sys-tems, even though they had not been subject to an adequate fundamen-tal investigation. Recent advances in model checking technology such as counterexample-guided abstraction refinement have put strong em-phasis 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 includ-ing 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