Algorithms for Reduced Ordered Binary Decision Diagrams (Q7361584)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry ROBDD
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Algorithms for Reduced Ordered Binary Decision Diagrams |
AFP entry ROBDD |
Statements
27 April 2016
0 references
Julius Michaelis
0 references
Max W. Haslbeck
0 references
Peter Lammich
0 references
Lars Hupel
0 references
Algorithms for Reduced Ordered Binary Decision Diagrams (English)
0 references
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.
0 references
