Algorithms for Reduced Ordered Binary Decision Diagrams

Julius Michaelis 🌐, Max W. Haslbeck 🌐, Peter Lammich 🌐 and Lars Hupel 🌐

April 27, 2016

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We present a verified and executable implementation of ROBDDs in Isabelle/HOL. Our implementation relates pointer-based computation in the Heap monad to operations on an abstract definition of boolean functions. Internally, we implemented the if-then-else combinator in a recursive fashion, following the Shannon decomposition of the argument functions. The implementation mixes and adapts known techniques and is built with efficiency in mind.


BSD License


Session ROBDD