We present the verification of the normalization of a binary decision diagram (BDD). The normalization follows the original algorithm presented by Bryant in 1986 and transforms an ordered BDD in a reduced, ordered and shared BDD. The verification is based on Hoare logics and is carried out in the theorem prover Isabelle/HOL. The work is both a case study for verification of procedures on a complex pointer structure, as well as interesting on its own, since it is the first proof of functional correctness of the pointer based normalization process we are aware of.

Online Copy

Available as PDF-File (279KB)

BibTeX Entry

@inproceedings{Ortner-Schirmer-TPHOL05, author={Veronika Ortner and Norbert Schirmer}, title={Verification of {BDD} Normalization}, booktitle="Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 2005", editor="J. Hurd and T. Melham", year=2005,publisher=Springer,series=LNCS,volume=3603,pages={261--277}}