next up previous
Next: Advanced Functionalities Up: Standard Functionalities Previous: Check for Transition Relation

Counterexamples Generation.

One of the most important functionalities of symbolic model checking is the ability to generate a counterexample for unsatisfied properties. The algorithms used in NUSMV as a basis to perform the computation of counterexamples are the same as those implemented in CMU SMV and are those presented in [24].

NuSMV <>