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
Topics
Session ROBDD
- Bool_Func
- BDT
- Option_Helpers
- Abstract_Impl
- Pointer_Map
- Middle_Impl
- Array_List
- Pointer_Map_Impl
- Conc_Impl
- Level_Collapse
- BDD_Examples
- BDD_Code