欢迎访问陈意云的主页

联系电话：0551-63607043（办）主页更新时间 2016.12.8


	个人简历
	陈意云，男，1946年生，教授，博士生导师。1965年毕业于合肥师范学院实验中学（其前身是安徽省科学技术学校），随后上山下乡当了13年知青。（回忆录：两次高考之间的十三年知青生涯—纪念上山下乡50周年）1978年考取中国科大，1980年专科毕业于中国科大，1982年12月研究生毕业于上海华东计算所，获硕士学位。1983年开始一直在中国科大计算机系工作，其中1989年到美国芝加哥大学访问两年。主讲《编译原理》、《程序分析和程序验证》和《程序设计语言理论》等课程。主持完成了七项国家自然科学基金面上项目以及若干其它项目。
	科研情况 1、主要研究方向：程序设计语言理论和实现技术、程序验证、软件安全等。目前正在执行的国家自然科学基金项目是（项目简介）：提高程序验证自动化程度的技术 2、科研项目网站（中科大－耶鲁高可信软件联合研究中心网站）：http://kyhcs.ustcsz.edu.cn/ 实验室介绍 3、部分已发表论文 4、联合研究中心新闻：201004 201106 201108 201110 201211 201306 201312 5、面向选择导师的研究生的介绍
	教学资源 1、《计算机科学导论》教学资源 2、《编译原理》教学资源 3、《编译原理高级教程》教学资源 4、《程序设计语言理论》教学资源 5、部分已编写教材

研究项目简介

1、提高程序验证自动化程度的技术

基于逻辑推理的程序验证是提高软件可信程度的一种重要方法。本项目研究促进程序验证方法走向实用的技术和相关理论，重点解决指针类型给程序验证带来的障碍，为指针程序的自动验证设计一种比较全面的解决办法。

该项研究基于下面的思路：（1）程序验证不必孤立地进行，可用程序分析收集的信息来支持程序验证；（2）程序员可通过提供一些对程序分析和程序验证有用的提示，来换取它们替程序员完成一些很有价值的事情；（3）在通过增强编程语言和断言语言的表达能力来拓展程序验证器的能力时，要尽量避免给自动定理证明器带来太多的负担。

本项目的研究基于上面的思路展开，预计主要亮点是：提出一种直接把形状图作为断言的形状图逻辑，提出形状系统概念。

本项目的研究帮助解决程序自动验证的瓶颈问题，促进程序验证的研究和应用的开展。

返回顶层

部分已发表论文

1、陈意云，Head Boudedness of Nonterminating Rewritings, J. of Computer Science and Technology, 1995, 10(3), pp. 281-284．

2、林洪、陈意云，Category Semantics of Gamma，Advanced Software Research, 1998.2, 5(1), pp. 78-88．

3、林洪、陈意云，Category Semantics of Higher Order Gamma，Advanced Software Research, 1998.8, 5(3), pp.267-278．

4、袁春、陈意云，进程创建的语义及等价性，计算机学报，23(8)，pp.877-881，2000.8．

5、袁春、陈意云，Software Architecture Evolution by Multiset Transformation, Proceedings of the International Conference on Software: Theory and Practice , the 16th IFIP World Computer Congress, Beijing , China , pp.236-243, 2000.8．

6、袁春、陈意云，Constraint-Preserving Architecture Transformations: A Graph Rewriting Approach, 16(6), Journal of Computer Science & Technology, pp.590-594, 2001.11．

7、郭帆、陈意云、胡荣贵，Machine Code Type Safety, 4^th International Conference on Formal Engineering Methods, Shanghai, China, LNCS 2495, pp.495-499, October 21-23. 2002．

8、郭帆、陈意云、胡荣贵，基于类型化内存地址的安全策略的设计与实现，计算机研究与发展，40(7)，pp.1001-1007，2003.7．

9、胡荣贵、陈意云、郭帆、张昱，基于类型注解的认证编译器的设计与实现，计算机研究与发展，41(1)，pp.28-33，2004.1．

10、袁春、陈意云，约束检查的最弱及增量前条件方法，计算机研究与发展，40(7)，pp.1088-2003，2003.7．

11、李永祥、陈意云，基于函数指针数组的代码迷惑技术，计算机学报，27(12)， pp.1706-1711，2004.12．

12、胡荣贵、陈意云、郭帆，机器语言的类型化及代码的安全检查，计算机研究与发展，计算机研究与发展，41(6)，pp.965-971，2004.6．

13、陈晖、陈意云、茹祥民，一种用于Java程序验证编译的标签类型，软件学报，16(3)，pp. 346-354，2005.3．

14、吴萍、陈意云、张健，并发Java程序同步操作的有效删除，软件学报，16(10)， pp.1708-1716，2005.10．

15、陈晖、陈意云、吴萍、项森，一种用于Java虚拟机的类型化低级语言，计算机研究与发展，43(1)，pp.15-22，2006.1．

16、吴萍、陈意云、张健，多线程程序数据竞争的静态检测，计算机研究与发展，43(2)，pp.329-335，2006.2．

17、付雄、张昱、陈意云，Data-Layout Optimization Using Reuse Distance Distribution. Emerging Directions in Embedded and Ubiquitous Computing EUC 2006 Workshops: NCUS, SecUbiq, USN, TRUST, ESO, and MSA, Seoul , Korea , Proceedings. Series: Lecture Notes in Computer Science, Vol. 4097, pages 858-867, August 1-4, 2006.

18、项森、陈意云、林春晓、李隆，Molularly Certified Dynamic Storage Allocation in SCAP.In Proceedings of Sixth International Conference on Quality Software (QSIC'06), pages 321-328, IEEE CS press, Oct. 2006.

19、项森、陈意云、林春晓、李隆，动态存储管理安全验证的Coq实现，计算机研究与发展，44(2)，pp.361-368，2007.2。

20、Yu Guo, Xinyu Jiang, Yiyun Chen, and Chunxiao Lin. A certified thread library for multithreaded user programs. In Proceedings of 1st IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, pages 117-126, IEEE CS press, June 2007.

21、Yiyun Chen, Lin Ge, Baojian Hua, Zhaopeng Li, and Cheng Liu. Design of a certifying compiler supporting proof of program safety. In Proceedings of 1st IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, pages 127-136, IEEE CS press, June 2007.

22、Chunxiao 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.

23、Chun-xiao Lin, Yi-yun Chen, Long Li, and Bei Hua. Garbage collector verification for proof-carrying code. Journal of Computer Science & Technology, Vol. 22, No. 3, pp. 426-437, June 2007.

24、CHEN Yiyun, GE Lin, HUA Baojian, LI Zhaopeng, LIU Cheng, WANG Zhifang. A pointer logic and certifying compiler. Frontiers of Computer Science in China , 1(3), pp. 297-312, 2007.8.

25、高鹰、陈意云，基于抽象解释的代码迷惑有效性比较框架，计算机学报，30(5)，pp.806-814，2007.5。

26、陈意云、华保健、葛琳、王志芳，一种用于指针程序安全性证明的指针逻辑，计算机学报，31(3)，pp.372-380，2008.3。

27、华保健、陈意云、李兆鹏、王志芳、葛琳，安全语言PointerC的设计及形式证明，计算机学报，31(4)，pp.556-564，2008.4。

28、李兆鹏、陈意云、葛琳、华保健，一种汇编程序的形式验证框架，计算机研究与发展，45(5)，pp.825-833，2008.5。

29、Zhifang Wang, Yiyun Chen, Zhenming Wang, Wei Wang and Bo Tian, An extension to Pointer Logic for verification, In Proceedings - 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, pages 49-56, IEEE CS press, Jun 17-19 2008.

30、郭宇、陈意云、林春晓，一种构造代码安全性证明的方法，软件学报，2008.10，19(10)，pp.2720-2727。

31、王志芳、陈意云、王振明、华保健，Automated verification of pointer programs in pointer logic Frontiers of Computer Science in China, 2(4), pages 380-397, 2008.12.

32、Long Li, Yu Zhang, Yi-yun Chen, and Yong Li. Certifying concurrent programs using transactional memory. Journal of Computer Science & Technology, Vol. 24, No. 1, pp. 110-121, January 2009.

33、王振明、陈意云、王志芳，用于指针逻辑的自动定理证明器，软件学报，2009.8，20(8):2037-2050。

34、陈意云、李兆鹏、王志芳、华保健，一种用于指针程序验证的指针逻辑，软件学报，2010.3，21(3):415-426。

35、梁红瑾、张昱、陈意云、李兆鹏、华保健，处理指针相等关系不确定的指针逻辑，软件学报，21(2):334-343，2010.2

36、张志天，李兆鹏，陈意云，刘刚，一个程序验证器的设计和实现，计算机研究与发展，50(5): 1044-1054, 2013

37、Zhao-Peng Li, Yu Zhang, and Yi-Yun Chen. A shape graph logic and a shape system. Journal of Computer Science & Technology, Vol. 28, No. 6, pp. 1063-1084, Nov. 2013. （中文版见形状图逻辑和形状系统）