Implication-Based Approximating Bounded Model Checking. - Zhenyu Chen 001; Zhihong Tao; Baowen Xu; Lifu Wang (FSEN, 2007)

QBF-Based Symbolic Model Checking for Knowledge and Time. - Conghua Zhou; Zhenyu Chen 001; Zhihong Tao (TAMC, 2007)

An evaluating indicator for urban sprawl simulation and prediction. - Jiangquan Hu; Zhihong Tao; Jing Chen; Zongmiao Kou; Lun Wu (Geoinformatics, 2010)