中文摘要：

Yu Guo is currently a post- doctoral researcher in Department of Computer Science ＆ Technology at University of Science ＆ Technology of China. He received his Ph.D. de- gree in computer science from Uni- versity of Science ＆ Technology of China in 2007. He is a member of China Computer Federation. His research interests involve language based software safety, system software verification, and con- current program verification. Xin-Yu Jiang is currently a Ph.D. candidate in Department of Computer Science ＆ Technology at University of Science ＆ Technology of China. He received his B.E. degree in computer science from University of Science ＆ Technology of China in 2005. His research interests involve language based software safety, pro- gram verification on assembly code level, and concurrent program verification. Yi-Yun Chen is a professor in Department of Computer Science Technology at University of Science ＆ Technology of China. He re- ceived his M.S. degree from East- China Institute of Computer Tech- nology in 1982. His research interests include applications of logic （in- cluding formal semantics and type theory）, techniques for designing and implementing programming languages and software safety and security.