BDD Normalisation

 

Title:	BDD-Normalisation
Author:	Veronika Ortner and Norbert Schirmer
Submission date:	2008-02-29
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.

 

Proof outline Proof document

Browse theories

Download this entry

Older releases: Isabelle 2009: afp-BDD-2009-04-29.tar.gz Isabelle 2008: afp-BDD-2008-06-10.tar.gz Isabelle 2007: afp-BDD-2008-03-07.tar.gz