Counterexample generation research in symbolic model checking based on OBDD
YAO Quanzhu, MIAO Yongjun
Computer Engineering and Applications . 2012, (10): 54 -58 .