中文摘要：

E-mail： {wj, xd.ma, wdong, wwliu}@nudt.edu.cn; relive007@163.com Ji Wang received his Ph.D. de- gree in computer science from Na- tional University of Defense Technol- ogy in 1995. He is currently a profes- sor at National Laboratory for Par- allel and Distributed Processing of China. His research interests include high confidence software and systems, software engineering and distributed computing. He is a senior member of China Computer Federation. Xiao-Dong Ma received his M.S. degree in computer science from Na- tional University of Defense Technol- ogy （NUDT） in 2004. He is currently a Ph.D. candidate in School of Com- puter, NUDT. His research interests are in the areas of program analysis and verification. Wei Dong received his Ph.D. de- gree in 2002 from National University of Defense Technology （NUDT）. He is currently an associate professor at National Laboratory for Parallel and Distributed Processing, and School of Computer, NUDT. His research in- terests include high confidence soft- ware engineering, software verifica- tion, software reliability and testing. Hou-Feng Xu received his B.S. degree in information and comput- ing science from Xi＇an Jiaotong Uni- versity in 2006. He is currently an M.S. candidate of computer science and technology in the National Uni- versity of Defense Technology. His research interests are in the areas of program analysis and verification. Wan-Wei Liu is currently a Ph.D. candidate in School of Com- puter, National University of Defense Technology. His research interests in- clude model checking and theorem proving.