联系电话:0551-3607043(办) E-mail:yiyun@ustc.edu.cn  主页更新时间 2010.5.23
     
 

个人简历

 

陈意云,男,1946年生,教授,博士生导师。1965年上山下乡当了13年农民,1978年考取中国科大,1980年专科毕业于中国科大,1982年12月研究生毕业于上海华东计算所,获硕士学位。1983年到中国科大计算机系工作,1989年到美国芝加哥大学访问两年。

    主讲编译原理、编译原理高级教程和程序设计语言理论等课程。主持完成了五项国家自然科学基金面上项目以及若干其它项目。

 

科研情况

1、主要研究方向:程序设计语言理论和实现技术、程序验证、软件安全等。

    目前正在执行的国家自然科学基金面上项目是 (项目简介):

    1、软件安全性的验证和编译

    2、面向携带证明软件设计的语言、逻辑和证明

2、科研项目网站:http://kyhcs.ustcsz.edu.cn/

3部分已发表论文

4中科大-耶鲁高可信软件联合研究中心简介

5面向选择导师的研究生的介绍

 

教学资源

1、《编译原理》教学资源

2、《编译原理高级教程》教学资源

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

4、 部分已编写教材

 

研究项目简介

1、软件安全性的验证和编译

本项目采用逻辑方法和类型方法相结合的方式,研究串行高级语言程序安全性的描述、证明、从高级语言级的安全性证明到目标语言级安全性证明的编译和在目标语言级进行安全性证明的检验的方法,解决该方法中主要的理论和技术问题,包括源语言的类型系统和逻辑系统的研究及它们的可靠性证明方法的研究、目标语言基础逻辑的研究、安全性证明的编译技术研究等。本项目还将实现出具证明编译器的一个原型,并将这种方式用于操作系统内核和嵌入式软件的设计。

 

2、面向携带证明软件设计的语言、逻辑和证明

本项目研究如何有效地集成形式程序验证和领域专用语言这两种软件技术,形成提高编写健壮软件生产力和提高对它们正确性和安全性信任程度的软件开发新方法,并构建基于此方法的开发携带证明大型系统软件的基础结构。

本项目具体研究以领域专用语言(DSL)为中心的开发携带证明程序的开放框架,研究支持DSL开发的统称为出具证明编程语言(CPL)的语言和工具,并以CPL为工具,验证操作系统内核和运行系统的关键部分。

这是一项为了把形式程序验证技术推向实用,解决其中理论和技术问题的奠基性研究。

返回顶层

 

部分已发表论文

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

返回顶层

 

《编译原理》教学资源

1、教材

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

    勘误表(2010.5.23)

2、讲稿(2010年)

    第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年试题

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

  1999-2002 2003 2004 2005 2006 2007 2008 2009

  报考硕士研究生参考信息

返回顶层

 

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

1、讲稿 (2010年)

    第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年改版的 部分章节书稿

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

2、讲稿(2006年)

    第1章 引言    第2章 可计算函数程序设计语言   第3章 泛代数和代数数据类型

    第4章 简单类型化l演算    第5章 类型化l演的模型  第6章 命令式程序

    第7章 多态性   第8章 子定型及有关概念  第9章 类型推断

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

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

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

返回顶层