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.

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: