Skip to main content.


BDDs [bry86,and97] (or more precisely ROBDDs) are efficient data structures for representing boolean formula. They are widely used in formal verification, in particular symbolic model-checking. The idea of symbolic model-checking is to represent sets of states transition relations as formula (and to compute the fix-point of the set of all reachable states for reachability analysis).

Buddy is a BDD library written in C with an API both in C and C++. It is developer friendly with a simple interface. It supports all standard BDD operations, variable ordering, printing, has automated garbage collection, and is compilable on Unix and Windows platforms. Ruby, despite being a scripting language, is a powerful and clean object-oriented language that is very easy to learn and use. In particular it is well-suited for quick prototyping and education purposes. Ruby-BDD is a binding for Ruby based on Buddy that provides BDD classes to create and manipulate BDDs in Ruby.

Maintainer: Alexandre David.


  • [bry86] Bryant E. Randal. Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, Vol. C - 35, No. 8, August, 1986, pp. 677 - 691.
  • [and97] Henrik Reif Andersen. An Introduction to Binary Decision Diagrams, Lecture notes.

Latest News

Ruby-BDD version 0.2 released

9 Aug 2006

Added support for bit vectors and finite domains.

Ruby-BDD version 0.1 released

23 May 2006

First release of the binding.