Symbolic forward image computation with BDDs. Compute exact reachable state sets without enumerating states explicitly — the engine behind early model checkers.
Part of Decision Procedures for Hardware Formal Verification on formal.org.