联系电话: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 GammaAdvanced Software Research, 1998.2, 5(1), pp. 78-88

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

4、袁春、陈意云,进程创建的语义及等价性,计算机学报,23(8)pp.877-8812000.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, 4th International Conference on Formal Engineering Methods, Shanghai, China, LNCS 2495, pp.495-499, October 21-23. 2002

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

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

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

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

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

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

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

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

16、吴萍、陈意云、张健,多线程程序数据竞争的静态检测,计算机研究与发展,43(2)pp.329-3352006.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-3682007.2

20Yu 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-8142007.5

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

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

28李兆鹏、陈意云、葛琳、华保健,一种汇编程序的形式验证框架,计算机研究与发展,45(5)pp.825-8332008.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.1019(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.321(3):415-426

35、梁红瑾、张昱、陈意云、李兆鹏、华保健,处理指针相等关系不确定的指针逻辑,软件学报,21(2):334-3432010.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. (中文版见形状图逻辑和形状系统

38、张昱、陈意云、李兆鹏:形状图理论的定理证明,计算机学报,39(12):2460-2480, 2016.12

待发表论文

1程序验证系统中断言语言的设计

2操作带附加链表的数据结构的程序的验证

返回顶层

《计算机科学导论》教学资源

1、教材

暂无

2、讲稿(2016年)

    课程简介   第一讲 代数等式理论的自动定理证明   第二讲 对程序进行推理的逻辑   第三讲 编程语言的类型系统

    第四讲 离散数学与计算机科学        第五讲 经典计算的计算模型            第六讲 计算复杂性和算法分析

    第七讲 面向计算机体系结构的程序优化        第八讲 多核体系结构与并行编程模型

    第九讲 新型计算模型和顺序交互的数学        第十讲 大数据的处理和分析

返回顶层

 

《编译原理》教学资源

1、教材

    陈意云、张昱,编译原理(第3版)(“十二五”普通高等教育本科国家级规划教材),高等教育出版社,2014

    陈意云、张昱,编译原理(第3版)习题精选与解析(“十二五”普通高等教育本科国家级规划教材配套参考书),高等教育出版社,2014

 2、讲稿(2011年)

    第1章 引论   第2章 词法分析   第3章 语法分析   第4章 语法制导的翻译   第5章 类型检查

    第6章 运行时存储空间的组织和管理   第7章 中间代码生成   第8章 代码生成

    第9章 独立于机器的优化   第10章 依赖于机器的优化   第11章 编译系统和运行系统

    第12章 面向对象语言的编译   第13章 函数式语言的编译

    课程实践项目    课程实践参考资料    课程实践需要用的源代码    课程实践安排    测试程序

3、参考书

    1、陈意云、张昱,编译原理习题精选与解析,高等教育出版社,2005.8

    前言  勘误表(2010.3.27)

    2、陈意云、张昱,编译原理(普通高等教育“十五”国家级规划教材),高等教育出版社,2003

    目录   勘误表(2007.3.30)

4、参考试题 (大部分答案请见《编译原理习题精选与解析》)

    1997年试题   1998年试题  1999年试题   2001年试题 2003年试题 2004年试题 2005年试题

    2006年试题  2007年试题   2008年试题    2009年试题     2010年试题

5考研参考题(大部分答案请见《编译原理习题精选与解析》)

  1999-2002 2003 2004 2005 2006 2007 2008 2009

  报考硕士研究生参考信息

返回顶层

 

《程序分析与程序验证》教学资源

1、讲稿 (2011年)

    第1章 引言    第2章 数据流分析(Nielson等)   第2章 数据流分析(补充)

    第3章 基于约束的分析(Nielson等)    第3章 基于约束的分析(补充)

    第4章 抽象解释(Nielson等)    第4章 抽象解释(补充)

    第5章 类型和效果系统(Nielson等)    第5章 类型和效果系统(补充)

    第6章 模型检测    第7章 程序验证(Necula, 1, 2, 3, 4

2、参考书

    1. F. Nielson, H. R. Nielson, and C. Hankin, Principles of Program Analysis, 2nd edition, Springer, 2005

    2. A. V. Aho, M. S. Lam, R. Sethi, and J. D. Ullman, Compilers: Principles, Techniques, and Tools , 2nd edition, Addison-Wesley, 2007

    3. M. Huth and M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, Second Edition, 2004

    4. http://www2.imm.dtu.dk/~riis/PPA/ppasup2004.html

返回顶层 

 

《程序设计语言理论》教学资源

1、教材

  陈意云、张昱,程序设计语言理论(第二版),高等教育出版社,2010

   目录  勘误表(2010.11.09)

    2010年改版的 部分章节书稿

    第1章 引言    第2章 泛代数和代数数据类型    第6章 递归类型

2、讲稿(2010年)

    第1章 引言    第2章 泛代数和代数数据类型     第3章 简单类型 化l演算

  第4章 类型 化l演算的模型     第5章 命令式程序的语义    第6章 递归类型

    第7章 多态性     第8章 依赖类型    第10章 子定型

3、参考书

    1. John C. Mitchell: Foundations for Programming Languages. The MIT Press, 1996

    2. Robert Harper: Practical Foundations for Programming Languages. A working draft is available at http://www.cs.cmu.edu/~rwh/plbook/book.pdf, 2009

    3. Banjamin C. Pierce, editor: Advanced Topics in Types and Programming Languages. The MIT Press, 2005

    4. Banjamin C. Pierce: Types and Programming Languages. The MIT Press, 2002

    5. John C. Mitchell: Concepts in Programming Languages. Cambridge University Press, 2002

返回顶层

 

部分已编写教材

1、陈意云,计算机科学中的范畴论,中国科大出版社,1993

2、陈意云,形式语义学基础,中国科大出版社,1994

3、陈意云、张昱,编译原理,高等教育出版社(普通高等教育“十五”国家级规划教材),2003

4、陈意云、张昱,编译原理习题精选与解析,高等教育出版社,2005

5、陈意云、张昱,编译原理,高等教育出版社(普通高等教育“十一五”国家级规划教材),2008

         勘误表(2011.3.13)

6张昱、陈意云,编译原理实验教程,高等教育出版社,2009.4.

7、陈意云、张昱,程序设计语言理论(第二版),高等教育出版社,2010.2.

8、张昱、陈意云,编译原理与技术,高等教育出版社,2010.8

      勘误表(2012.03.12)     PL/0编译器源代码及测试程序     课程实践的一种方案

9、 陈意云、张昱,编译原理(第3版) ,高等教育出版社(“十二五”普通高等教育本科国家级规划教材),2014

10、陈意云、张昱,编译原理(第3版)习题精选与解析,高等教育出版社(“十二五”普通高等教育本科国家级规划教材配套参考书),2014

返回顶层