中文摘要：

Xiaoxiao Yang got her PhD degree from Xidian University in 2009. She is now an assistant professor in State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences. Her main research interests are in the areas of concurrent theory, temporal logic, logic programming, software modeling, and verification.E-mail： xxyang@ios.ac.cn Yu Zhang got his PhD degree from 6cole Normale Superieure de Cachan, France in 2005 and has been an associate research professor of Institute of Software, Chinese Academy of Sciences since 2009. His research interests include formal methods, concurrent systems, information security, and programming languages. Ming Fu got his PhD degree from University of Science and Technology of China in 2009. He is currently a post- doctoral researcher in USTC-Yale Joint Research Center for high-confidence software, University of Science and Technology of China. His main research interests lie in the areas of forreal methods, concurrent program verification, and concurrency theory. Xinyu Feng got his PhD degree from Yale University in 2007. He is now a professor in computer science at University of Science and Technology of China. His research interests are in the area of formal program verification. In particular, he is interested in developing theories, programming languages and tools to build formally certified system software, with rigorous guarantees of safety and correctness