Many symbolic model checkers use \emph{Binary Decision
Diagrams} (BDDs) to efficiently determine whether two Boolean formulas
are semantically equivalent. For realistic problems, the size of the
generated BDDs can be enormous, and constructing them can easily become
a performance bottleneck. As a result, most state-of-the-art BDD
programs are written as highly optimized imperative C programs,
increasing the risk of soundness defects in their implementation. This
paper describes the use of \emph{monadic interpreters} to formally
verify BDD algorithms at a higher level of abstraction than the original
C program, but still at a concrete enough level to retain their
essential imperative features. Our hope is then that verification of
the original C program can be achieved by strictly localized refinement
reasoning.
During this work we encountered the surprising fact that modeling
imperative recursive algorithms monadically often results in logical
functions that are both partial and nestedly-recursive in their (hidden)
state parameters, making termination proofs difficult.