| 联系电话：0551-3607043（办） E-mail：yiyun@ustc.edu.cn 主页更新时间 2010.5.23 | |||||||||||||
|
|||||||||||||
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 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,
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-1007，2003.7．
9、胡荣贵、陈意云、郭帆、张昱，基于类型注解的认证编译器的设计与实现，计算机研究与发展，41(1)，pp.28-33，2004.1．
10、袁春、陈意云，约束检查的最弱及增量前条件方法，计算机研究与发展，40(7)，pp.1088-2003，2003.7．
11、
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
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、项森、陈意云、林春晓、
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
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
25、高鹰、陈意云，基于抽象解释的代码迷惑有效性比较框架，计算机学报，30(5)，pp.806-814，2007.5。
28、李兆鹏、陈意云、葛琳、华保健，一种汇编程序的形式验证框架，计算机研究与发展，45(5)，pp.825-833
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、陈意云、李兆鹏、王志芳、华保健，一种用于指针程序验证的指针逻辑，软件学报
《编译原理》教学资源
1、教材
陈意云、张昱，编译原理（普通高等教育“十一五”国家级规划教材），高等教育出版社，2008
2、讲稿（2010年）
第1章 引论 第2章 词法分析 第3章 语法分析 第4章 语法制导的翻译 第5章 类型检查
第6章 运行时存储空间的组织和管理 第7章 中间代码生成 第8章 代码生成
第9章 独立于机器的优化 第10章 依赖于机器的优化 第11章 编译系统和运行系统
第12章 面向对象语言的编译 第13章 函数式语言的编译 课程设计安排
3、参考书
1、陈意云、张昱，编译原理习题精选与解析，高等教育出版社，2005.8
2、陈意云、张昱，编译原理（普通高等教育“十五”国家级规划教材） ，高等教育出版社，2003
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、参考书
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.
1、教材
陈意云、张昱，程序设计语言理论（第二版），高等教育出版社，2010
目录 勘误表（暂无)
2010年改版的 部分章节书稿
第1章 引言 第2章 泛代数和代数数据类型 第6章 递归类型
2、讲稿（2006年）
第1章 引言 第2章 可计算函数程序设计语言 第3章 泛代数和代数数据类型
第4章 简单类型化l演算 第5章 类型化l演的模型 第6章 命令式程序
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、
6、张昱、陈意云，编译原理实验教程，高等教育出版社，2009.4.
7、陈意云、张昱，程序设计语言理论（第二版），高等教育出版社，2010．
