Algorithms for Reduced Ordered Binary Decision Diagrams

Julius Michaelis, Maximilian P. L. Haslbeck, Peter Lammich and Lars Hupel

27 April 2016


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

Depends On

Used by


Related Entries