Tilbage til hovedside

BuDDy - A Binary Decision Diagram Package

Version 2.2

By Jørn Lind-Nielsen
Mail to: buddy@itu.dk

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!


The source code with documentation can be downloaded here:  buddy22.tar.gz  (440k)
BTW: I would apreciate any information on what projects BuDDy gets involved in (just curious).

Projects With BuDDy

Other information
More general information on BDDs can be found in Henrik Reif Andersen's BDD notes.
Other BDD packages are:

Questions can be sent to buddy@itu.dk. This page was last updated January 7th 2003.