The size and complexity of software and hardware systems have significantly
increased in the past years. As a result, it is harder to guarantee their
correct behavior. One of the most successful methods for automated verification
of finite-state systems is model checking. Most of the current model-checking
systems use binary decision diagrams (BDDs) for the representation of the
tested model and in the verification process of its properties. Generally, BDDs
allow a canonical compact representation of a boolean function (given an order
of its variables).