Authors: Veronika Ortner, Norbert Schirmer
Title: Verification of BDD-Algorithms in Isabelle/HOL
Abstract: 
We present the verification of the normalisation of a binary decision diagram 
(BDD).
The normalisation 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 normalisation process we are aware of.