近期研究成果
1、近5年连续承担国家自然科学基金面上项目：
• 基于语言理论和实现技术的移动代码安全（Security of mobile code based on techniques of programming language theory and implementation）
• 类型论在软件安全方面的应用研究（Application Research of Type Theory in Software Security and Safety）
• 软件安全性的验证和编译（Verification and Compilation of Software Safety）
• 面向携带证明软件设计的语言、逻辑和证明（Languages, Logics, and Proofs for Certified Software Design）
2、近5年在编程语言理论及实现技术、软件安全和软件验证方面培养了14名博士，其中在Intel、Microsoft和Sun等公司研发部门工作的有6人，在高校当教师的有6人，做博士后的有2人。
3、近期发表的代表性论文如下：
[1] X. Feng, Z. Shao, A. Vaynberg, S. Xiang, and Z. Ni. Modular verification of assembly code with stack-based control abstractions. In Proc. 2006 ACM Conference on Programming Language Design and Implementation, pages 401-414, June 2006.
[2] Chunxian Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, and Yu Guo. Foundational typed assembly language with certified garbage collection. In Proceedings of 1st IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, pages 326-335, IEEE CS press, June 2007.
[3] X. Feng, Z. Ni, Z. Shao, and Y. Guo. An open framework for foundational proof-carrying code. In Proc. 2007 ACM SIGPLAN International Workshop on Types in Language Design and Implementation, pages 67-78, Jan. 2007.
[4] A. McCreight, Z. Shao, C. Lin, and L. Li. A General Framework for Certifying Garbage Collectors and Their Mutators. In Proc. 2007 ACM Conference on Programming Language Design and Implementation, pages 468-479, June 2007.
[5] X. Feng, Z. Shao, Y. Dong, and Y. Guo. Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. In Proc. 2008 ACM Conference on Programming Language Design and Implementation, pages 170-182, June 2008.
[6] X. Feng, Z. Shao, Y. Guo and Y. Dong. Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. In Proc. Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments, October 2008.