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!

 Highlights

• All standard BDD operations (and, or, ite, replace, quantification, support, compose etc.)
• Many highly efficient vectorized BDD operations.
• Dynamic variable reordering.
• Dumps BDD as input for the graph printing program DOT.
• Lots of printing functions.
• Automated garbage collection.
• A C++ interface with automatic reference counting.
• An interface for encoding integer values and arithmetics with BDDs.
• Compiles on both Unix and Windows NT/9x platforms.

Projects With BuDDy

• Stepwise CTL Model Checking of State/Event Systems
• Verification of Hierarchical State/Event Systems using Reusability and Compositionality.
• Verification of Large State/Event Systems using Compositionality and Dependency Analysis
• Portland State University BDD course spring 2000
• STEP - The Stanford Temporal Prover
• Visual Software Homepage
• IBEN - Interactive BDD Environment
• UCLID: A Verification Tool for Infinite-State Systems

• Fabio Somenzis's CUDD  from Colorado University.
• Armin Biere's ABCD package
• Geert Janssen's  BDD  package from Eindhoven University of Technology.
• Carnegie Mellon's  BDD  package.
• The  CAL  package from Berkeley.
• K. Milvang-Jensen's parallel package BDDNOW .
• Bwolen Yang's PBF package.

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