next up previous
Next: Bibliography Up: Conclusions Previous: NUSMV is open: the

Future Directions

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

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 <>