The kernel provides the low level functionalities such as dynamic memory allocation, and manipulation of basic data structures (e.g., cons cells, hash tables). The kernel also provides all the basic BDD primitives, which are actually taken from the CUDD [57] BDD package. The CUDD package is a very complete BDD package, freely available on the web. It provides all the basic BDD operations, plus a series of advanced BDD functionalities (such as various state of the art BDD variable reordering algorithms, the possibility of grouping together variables in such a way that the reordering algorithms treats them as a single element, algorithms to perform BDD minimization, approximation and decompositions, ...). The CUDD package is integrated in NUSMV with a precisely defined interface. This makes it possible to replace the CUDD package with other state of the art BDD packages developed in the future, or with commercial BDD packages (such as the TiGeR [30] BDD package). The NUSMV kernel can be used as a black box, following coding standards that have been precisely defined.
>