Verification of BDD normalization
THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS（2005）
摘要
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.
更多查看译文
关键词
normalization process,functional correctness,binary decision diagram,complex pointer structure,hoare logic,bdd normalization,case study,theorem prover,original algorithm,model checking,state space,boolean function
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要