### 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

- Computer science/Algorithms
- Computer science/Data structures

### 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

### Depends on

- Automatic Data Refinement
- Collections Framework
- Native Word
- The Imperative Refinement Framework

### Used by

- Simplicial Complexes and Boolean functions

### Auto-related entries

- Simplicial Complexes and Boolean functions
- A Verified Proof Checker for Metric First-Order Temporal Logic

## Cite

×

ROBDD-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Apr 27, 2016 : Isabelle2016