I was wondering if you have considered creating a
parallel multithreaded version of your package?
My grad student has used it to verify properties about
Discrete-event systems (represented as automata). He
used it on a syatem at least 10^15 states. It used
about 100MB, but ran for several days without completing.
For large systems, speed rather than memory can be an
issue. I've seen a few papers on parallel version for
BDDs. Such a version could be useful.