何积丰

电子邮件： jifeng@iist.unu.edu

详细信息： http://www.iist.unu.edu/~jifeng/








简要经历
1960.05 ~ 1965.02 上海复旦大学数学系学习
1980.07 -~1981.07 美国坦福大学、旧金山大学进修
1965.03 -~1985.07 华东师范大学助教、讲师
1984.12 ~ 1998.07 英国牛津大学客座教授、高级研究员
1986.08 ~ 华东师范大学教授
1988 ~ 国家有突出贡献中青年专家；
1995.08 ~ 华东师范大学博士生导师；
1998.07 ~ 联合国大学国际软件技术研究所高级研究员
1996.08 ~ 上海交通大学兼职教授、博士生导师
1998.08 ~ 南京大学兼职教授、博士生导师
2001.11 ~ 华东师范大学软件学院院长
2002.12 ~ 华东师范大学终身教授
2003.05 ~ 浙江大学兼职教授、博士生导师

获奖情况
电子工业部软件一等奖（1985）
上海市科技进步一等奖（1986）
英国先进技术女皇奖（1989）
英国先进技术女皇奖（1993）
上海市科技进步一等奖（2000）
国家自然科学二等奖（2002）

代表论著



自1985年以来，在“设计严格安全软件的完备演算系统”方面的研究成果。主要提供了两项技术：（1）建立程序和软件规范的演算系统，在软件开发周期各个重要阶段，均可使用数学演算来支持建立软件设计的技术文档和验证任务；（2）设计完整的演算法则用来指导以下开发任务：①从用户需求导出软件系统各部件的规范说明；②从部件的规范说明演算出低层软件模块过程的功能说明。研究论文发表在“Comm of the ACM”、“Formal Aspect of Computing”、“Science of Computer Programming”、“Acta Information”等国际著名杂志及重要学术会议上，至2002年，被SCI它引169次。

1. J. He, J. He, C.A.R. Hoare, J.W. Sanders，Data Refinement Refined - Resume，Lecture Notes in Computer Science，1986，213: 187-196
2. C.A.R. Hoare, He Jifeng, J.W. Sanders，Prespecification in Data Refinement，Information processing Letters，1987，25: 71-76
3. He Jifeng，Process Simulation and Refinement，Formal Aspects of Computing，1989，1: 229-241
4. He Jifeng, C.A.R. Hoare，From Algebra to Operational Semantics，Information processing letters，1993，45: 75-80
5. He Jifeng，From CSP to Hybrid Systems，A Classical Mind，1994，171-191
6. He Jifeng, C.A.R. Hoare，Provably Correct Systems，Lecture Notes of Computer Science，1994，863: 288-335
7. He Jifeng，Provably Correct Systems: Modelling of Communication Languages and Design of Optimized Compilers，McGraw-Hill Publisher，1994.
8. He Jifeng, K. Seidel, A. McIver，Probabilistic Models for The Guarded Command Language，Science of Computer Programming，1997，28: 171-192
9. C.A.R. Hoare, He Jifeng，Unifying Theories of Programming，Prentice Hall International，1998.
10. He Jifeng，A Common Framework for Mixed Hardware/Software Systems，Proceedings of IFM"99，1999，1-24.

主要成就

1．提出数据精化的完备理论针对当时数据精化方法上存在不完备以及只能处理确定性程序语言等缺陷，何积丰和合作者在论文“Data Refinement Refined”和“Prespecification in Data Refinement”中给出了一个处理非确定程序语言数据精化的方法，使用“上下仿真映照对”来获得程序模块中各过程的函数说明，给出了完备演算规则。1989年，他与合作者指出了精化方法与程序代数定律的直接联系，从而可根据不同的语言选择相应的精化计算方法。欧洲著名规范语言B采用了该方法（见J-R Abrial专著The B Book第501页、第550页, 剑桥大学出版）。剑桥大学理论计算机科学丛书曾指出，这一数据精化完备理论是面向模型软件开发的一个里程碑。

2．建立程序和软件规范的统一数学模型 1986年，他与合作者提出了程序分解算子，并将规范语言与程序语言看成是同一类数学对象。 1987年，他在“The Weakest Prespecification”中提出可采用“关系代数”作为程序和软件规范的统一数学模型，并在此数学框架中发现求解规范方程（X；Q＞S）和（P；X＞S）的演算法则，这样使得关系代数可用来描写程序的分解和组合过程，因而数学方法可直接用于支持软件的开发。在上述工作基础上，提出了程序的代数定律理论，给出了程序设计语言的一套完备的代数定律，这使得程序变换可直接依赖于基本定律的应用来完成。

3．提出编程统一理论和连接各类程序理论的数学法则 1998年，他和C.A.R.Hoare在专著“Unifying Theories of Programming”中给出了能描述串行语言、并行语言、通信语言、逻辑语言、函数程序语言的统一数学模型，证明了三类不同语义（指称语义、代数语义和操作语义）的一致性，并提出“Linking Theory”应用于设计概率程序语言的数学模型。

4．用形式化界面理论沟通几种程序语言，提出非确定性数据流的数学模型和代数定律在1989年开始的欧洲尤里卡基础研究项目PROCOS中，其重要任务就是以形式化的界面理论来沟通几种程序语言及设计一个可证明的编译程序和程序变换系统。何积丰在项目中作出了重要贡献，他的专著Provable Correct Systems:Modelling of Communication Languages and Design of Optimized Compilers 总结了相关工作。1990年他在论文“A theory of Synchrony and Asynchrony”中提出了非确定性数据流的数学模型及代数定律，这套理论用于支持Jackson开发方法和异步通信进程设计。

5、研究软硬件协同设计系统的数学模型 1992年至今一直从事基于工业设计语言VERILOG的软硬件协同设计框架，讨论语言的仿真器语义和合成语义的一致性问题，设计具有最优配置的软硬件分解器和合成器的数学模型。现已开发完成“海神”软硬件协同设计平台并应用。

近期项目

2001 - 2003，VERILOG仿真器和合成器设计，上海市信息委项目（CX20010005）
2002 - 2004，UML软件开发进程的形式化理论，教育部重点项目(02104)
2003 - 2005，安全软件理论与软硬件协同设计，“211”项目
2002 - 2007，网构软件形式化理论与方法研究，973项目（Internet环境下基于Agent的软件中间件理论和方法的研究，课题编号：2002CB31200001）