The BDD package presented here was made as part of a ph.d. project on model checking of finite state machines. The package has evolved from a simple introduction to BDDs to a full blown BDD package with all the standard BDD operations, reordering and a wealth of documentation. The package is extremely simple to use; for C/C++ programs you just include "bdd.h" and link with "bdd" and then you are up and running. With the C++ interface you don't even have to think about reference counting and garbage collection.
BuDDy has been used succesfully to verify finite state machine systems with up to 1400 concurrent machines working in parallel (see the paper "Verification of Large State/Event systems Using Compositionality and Dependency Analysis", Tools and Algorithms for the Construction and Analysis of Systems '98 (TACAS'98). LICS 1384, Springer-Verlag).
Projects for integrating BuDDy with both Moscow ML and New Jersey ML have resulted in really efficient BDD operations in ML. See the MuDDy page for more information. BuDDy is now also part of the HOL theorem prover!
Projects With BuDDy
Questions can be sent to firstname.lastname@example.org. This page was last updated January 7th 2003.