We have presented the NUSMV symbolic model checker. The NUSMV architecture provides a precise distinction from the back-end (model checking algorithms, heuristics for optimal conjunctive partitioning, ...) and the front-end (the input language). The NUSMV back-end is general purpose, and can be used not only for verifying hardware but also for the verification in other fields in which systems can be modeled as an FSM (e.g., software,...).
The rest of this section compares the performance of NUSMV and CMU SMV, describes the development of a planner built on top of NUSMV, and some directions for future developments.
>