LNCS 2772 - Counterexamples Revisited: Principles ...

Counterexamples Revisited: Principles , Algorithms, applications Edmund Clarke1and Helmut Veith21 School of Computer Science, Carnegie Mellon University, f ur Informationsysteme, Technische Universit at Wien, counterexample generation is a central featureof model checking which sets the method apart from other approachessuch as theorem proving. The practical value of Counterexamples tothe 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 suchas counterexample-guided abstraction refinement have put strong em-phasis on Counterexamples , and have lead to renewed interest both infundamental and pragmatic aspects of counterexample generation.

state-of-the-art model checking systems. In Section 5 we survey user-oriented applications of counterexamples in dif-ferent frameworks, most notably in software verification, where ordinary coun-terexamples are only part of a more complex debugging process. 2 Temporal Logic Model Checking in …

Loading..

Tags:

  Applications, Principles, Model, Checking, Model checking

Information

Related search queries