Verifying BDD Algorithms through Monadic Interpretation

Verifying BDD Algorithms through Monadic Interpretation
Sava Krstic and John Matthews

Many symbolic model checkers use 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 monadic interpreters to formally verify BDD algorithms at a higher level of abstraction than the original C program, but stilll at a concrete enough level to retain their essential imperative features. Our hope is then that verification of the original C program can be acheived 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.

Mon Feb 4 13:08:50 EDT 2002