Next: Bounded CTL.
Up: System Functionalities
Previous: Counterexamples Generation.
NUSMV provides advanced model checking functionalities, including
specialized algorithms for the verification of invariants, and
heuristics aiming at the reduction of the state explosion problem. In
the following these functionalities are briefly explained.
NuSMV <
>