Algorithms for Reduced Ordered Binary Decision Diagrams

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

April 27, 2016

Abstract

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.

License

BSD License

Topics

Session ROBDD

Depends on

Used by

Cite

× 
@article{ROBDD-AFP,
  author  = {Julius Michaelis and Max W. Haslbeck and Peter Lammich and Lars Hupel},
  title   = {Algorithms for Reduced Ordered Binary Decision Diagrams},
  journal = {Archive of Formal Proofs},
  month   = {April},
  year    = {2016},
  note    = {\url{https://isa-afp.org/entries/ROBDD.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: