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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Ortner, V., & Schirmer, N. (2005). Verification of BDD normalization. In Lecture Notes in Computer Science (Vol. 3603, pp. 261–277). Springer Verlag. https://doi.org/10.1007/11541868_17
Mendeley helps you to discover research relevant for your work.