Verification of BDD Normalization

Veronika Ortner and Norbert Schirmer

Paper on the TPHOLs 2005 --- 18th International Conference on Theorem Proving in Higher Order Logics , August 22-25, 2005, Oxford, UK


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

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",

Norbert Schirmer
Last modified: Tue Oct 31 10:52:03 MET 2006