[  download | license | background ]

Download

[ abcd-0.3.tar.gz ]

This is the compact BDD library ABCD, which is the standard BDD backend for our mu-calculus model checker Mucke.

License

ABCD is a absolutely free software. It can be used and changed in any way you like.

Background

During the design of ABCD we wanted to experiment with some new techniques for implementing a BDD library. The main difference to other BDD library is the minimalistic representation of individual nodes. In particular ABCD only requires two 32 bit words for each node. The library also tries to maximize the available memory for the BDD cache. No dynamice variable reordering is implemented and probably not even possible to implement with the current scheme without increasing the size of nodes considerably.

ABCD was very competetive in an evaluation of different BDD libraries for model checking organized by Bwolen Yang. There is also a paper about this evaluation. Bwolen has some more pages on this subject.

Finally the BDD-Portal contains more information on BDDs in general. There you can also find a very informative comparison of publically available BDD packages compiled by Geert Jansen.