To make the system more usable and improve its efficiency and its expressiveness there are plans to introduce the following additional functionalities.

- A simulation functionality, which allows the user to acquire confidence with the correctness of the model before the verification of the properties.
- A sequential input language. The problem with the NUSMV language is that it is most amenable for hardware and hardware-like systems, while its ability to model software systems is left to the user. This leaves the user with the burden of a complex model generation activity. In general this can be hardly acceptable, as many specification languages (e.g., SDL) are intrinsically sequential. A possible new input language for NUSMV is VERUS [13].
- Forward CTL model checking. In symbolic model checking, CTL
formulas are evaluated backward (the base operation is
**EX**, see Section 2). New algorithms have been developed that allow performing evaluation of CTL formulas via a forward state traversal [43]. These algorithms allow for the verification of large systems that cannot be handled by the classical backward algorithms. - Cone of influence reductions [3]. The idea is to simplify the model w.r.t. the cone of influence of the formula to be verified, thus reducing the search space.
- Use of ``reachability don't cares'' (RDC) [63] to reduce the cost of CTL model checking.
- High density reachability analysis [54] and under and over approximate reachability analysis [48]. These have shown in some cases, together with RDC, dramatic effects in the performance of CTL model checking.
- Optimizations for constraint-rich models [62], to enable the verification of systems with complex time-invariant constraints.

Some lines of research that are currently under study and whose results we plan to integrate inside NUSMV are specific reduction techniques for sequential systems, a set of abstraction techniques that implement certain heuristics developed in the theorem proving community [38] and that we believe will be very effective, the extension of CTL model checking to multi-agent systems and security applications [2], and the integration of model checking and theorem proving (SAT in particular) following the ideas reported in [36] and in [5].

NuSMV <>