Verifying BDD Algorithms through Monadic Interpretation
VMCAI, pp. 182-195, 2002.
monadic interpretationhigher levelessential imperative featurestate-of-the-art bdd programbdd algorithmMore(8+)
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 wr...More
Full Text (Upload PDF)
PPT (Upload PPT)