何积丰从复旦大学数学系毕业，并被分配到华东师范大学工作，先后担任教授、博士生导师；1980年被派往美国旧金山大学进修；1984年在英国牛津大学计算机实验室任客座教授、高级研究员；1998年担任联合国大学国际软件技术研究所高级研究员；2001年担任华东师范大学软件学院院长；2002年成为华东师范大学首批终身教授；2005年当选中国科学院院士；2010年被英国约克大学授予荣誉博士学位；2016年受聘为华东师范大学计算机科学与软件工程学院院长 [2]。2019年受聘为同济大学特聘教授，入职同济大学交通运输工程学院 [3-4]。
- 中文名
- 何积丰
- 外文名
- Ji-feng He
- 国 籍
- 中国
- 出生地
- 上海市
- 出生日期
- 1943年8月5日
- 毕业院校
- 复旦大学
- 职 业
- 教育科研工作者
- 代表作品
- Unifying Theories of Programming [18]
- 主要成就
- 2005年当选中国科学院院士
- 性 别
- 男
人物经历
播报编辑
1943年8煮朽市戒月5邀盛枣日，何积丰循钻出生于上海市捉榜。
1965年2月，何积丰从复旦大学数学棕鸦匪系毕业，并被分配到华东师范大学工作，是上海高校中第一批从事计算机科学研究的人员。
1海阿影9厚端踏80年7月，何积丰作为访问学者，被华东师范大学被派往美国旧金山大学进修，专攻计算机应用，课余时间里，他常常到远离旧金山的斯坦福大学和另一所名牌大学去旁听课程，斯坦福大学的导汽询师被他打动，不久，何积丰被批准进入斯坦福大学学习（至1981年7月）。
1984年12月，何积丰在英国牛津大学计算机实验室任客座教授、高级研究员（至1998年7月）。
1995年8月，何积丰被聘为华东师范大学博士生导师。
1998年7月，何积丰任联合国大学国际软件技术研究所高级研究员。
2001年11月，何积丰担任华东师范大学软件学院院长。
2002年12月，何积丰成为华东师范大学首批终身教授。
2005年，何积丰当选中国科学院院士。
2016年，何积丰受聘为华东师范大学计算机科学与软件工程学院院长。
2019年，何积丰受聘为同济大学特聘教授，入职同济大学交通运输工程学院 [19-20]。
主要成就
播报编辑
科研成就
- 科研综述
①创建程序统一理论，奠定了软件语义元理论基础，开创了软件理论的新学派。
何积丰与图灵奖获得者Hoare教授创造性地提出了软件的程序统一理论，解决了程序语义的一致性问题，奠定了软件语义元理论基础，开创了程序统一理论学派，出版了英文专著《Unifying Theories of Programming》，该文献他引超过800次。程序统一理论已被国际上公认为研究各类程序语言的一种标准方法。自2006年起，每两年举办一次程序统一理论国际学术研讨会，包括牛津大学、约克大学、巴黎11大等在内的世界著名研究机构从事序统一理论的相关研究。
②创新软件开发方法学，建立了数据精化完备理论，被国际上誉为“面向模型软件开发的一个里程碑”。
针对软件开发各阶段模型正确性问题，何积丰创建了数据精化完备理论，首次提出了数据精化的“程序分解算子”与“上下仿真映照对”方法，将规范语言与程序语言看成是同一类数学对象，采用“关系代数”作为程序和软件规范的统一数学模型，在此框架中建立了求解规范方程的演算法则。该成果被国际计算机科学界誉为“面向模型软件开发的一个里程碑”。
③开拓可信嵌入式软件设计理论与技术，促进了方法与技术在安全攸关行业领域的应用。
何积丰创造性地开拓和发展了基于模型的可信软件开发与验证研究领域，建立了正确性系统的可证理论与方法，解决了可信嵌入式系统构造与验证技术的若干关键问题，并应用于轨道交通、汽车电子、航天控制等安全攸关行业，推动了相关产业发展。 [18]
二零一七年香山科学会议，何积丰在世界上首次提出“可信人工智能”，自此世界各地开始广泛关注人工智能的安全可信问题。 [29]
- 学术论著
截至2018年，何积丰出版英文专著2部，在国际期刊和会议上发表论文160余篇，他引4000余次 [6]。
He Jifeng and C.A.R. Hoare. "Algebraic specification and proof of a distributed recovery algorithm" Distributed Computing Vol 2, 1-12, (1987) [33]
He Jifeng and C.A.R. Hoare. "Categorical Semantics of Programming Language". Invited talk in Workshop of the mathematical foundation of semantics of programming languages, U.S.A. 1988. Lecture Notes in Computer Sciences 442. Springer, (1990) [34]
He Jifeng. "Hybrid Parallel Programming and Implementation of Synchronised Communication" Lecture Notes of Computer Science 711, 537-547, Springer, (1993) [35]
He Jifeng. "A Predicative Semantics for the Refinement of Real-time Systems" Lecture Notes of Computer Science 802, 230-249, Springer, (1994) [39]
He Jifeng and C.A.R. Hoare. “Linking theories in probabilistic programming” Information Sciences, vol 119, 205-218, (1999) [36]
He Jifeng "An Algebraic Approach to Verilog Programming" Lecture Notes in Computer Science 2757, 65-81, (2002) [40]
He Jifeng and Xu Qiwen. "Advanced features of Duration Calculus and their applications in sequential hybrid programs" Formal Aspect of Computing Vol 15, 84-99, (2003) [37]
He Jifeng "Linking theories of concurrency" (Invited talk) In Proceedings of CSP'25, Springer, (2004) [42]
Jifeng He, Jeff W. Sanders: Unifying Probability. UTP 2006: 173-199 [41]
Jifeng He, Qin Li: A new roadmap for linking theories of programming and its applications on GCL and CS Science of Computer Programming 162 (2018) 3–34 [38]
- 承担项目
截至2020年，何积丰先后担任国家自然科学基金委重大研究计划、科技部973计划、863计划主题项目首席科学家，领衔国家自然科学基金委创新研究群体 [6]。
时间 | 项目名称 | 项目来源 |
|---|---|---|
2001年—2003年 | VERILOG仿真器和合成器设计 | 上海市信息委项目（CX20010005） |
2002年—2004年 | UML软件开发进程的形式化理论 | 教育部重点项目（02104） |
2002年—2007年 | 网构软件形式化理论与方法研究 | |
2003年—2005年 | 安全软件理论与软硬件协同设计 | “211”项目 |
2007年-2010年 | 海量信息的协同性和可生存性的理论与实践 | 国家科技部973计划 [30] |
2007年 | 可信软件基础研究 | 国家自然科学基金委员会 [25] |
2007年 | 计划信息物理融合系统主题项目 | 国家科技部863计划 [18] |
2017年-2019年 | 工业互联网，物联网安全操作系统产业化及规模化应用 | 国家工信部 [32] |
2020年-2023年 | 人工智能安全可信理论及验证平台 | 科技创新2030 [31] |
- 科研成果奖励
截至2020年，何积丰先后以唯一完成人获得国家自然科学奖二等奖和上海市科技进步奖一等奖各1项，以项目第一完成人荣获上海市科技进步奖特等奖 [26]，以第一完成人获省部级科技进步奖与科技成果奖一等奖4项 [6]。
时间 | 项目名称 | 奖励名称 |
|---|---|---|
1985年 | 电子工业部软件一等奖 | |
1986年 | 上海市科技进步一等奖 | |
2000年 | 设计严格安全软件的完备演算系统 | 上海市科技进步一等奖 [7] |
2002年 | 设计严格安全软件的完备演算系统 | 国家自然科学二等奖 [8] |
2012年 | 基于模型的可信软件理论与开发方法 | 教育部高等学校科学研究成果奖（自然科学）一等奖 [27] |
2013年 | - | 何梁何利基金科学与技术进步奖 [27] |
2014年 | 高端软件人才的协同创新培养模式 | 高等教育上海市教学成果奖特等奖 [27] |
2017年 | 面向综合能力提升的卓越软件人才培养体系 | 上海市教学成果奖一等奖 [27] |
2018年 | 逻辑思维与工具实践并重的跨领域可信软件人才培养模式 | 国家级教学成果奖二等奖 [27] |
2020年 | 面向重大工业装备核心控制软件的安全可信保障技术及应用 | 上海市科技进步特等奖 [27] |
人才培养
- 教育思想
何积丰努力践行服务社会的创新人才培养理念，始终坚持以科学的态度从事教学、科学研究服务并反哺教学，强调对青年道德品性的培养。他探索软件人才培养和科学研究的新路子，倡导“以学生为中心，以市场为导向，以创新求发展”的国际化办学理念，并构建了新颖的创新型软件人才分层培养一体化机制 [6] [9]。
- 讲授课程
何积丰为本科生开设了第一门由院士主讲的通识教育课程《计算机文化》，并梳理了自己多年的科研成果，为研究生开设了《程序统一理论》课程 [10]。
- 教学成果奖励
2006年何积丰获得上海市教学名师称号，2013年9月获得第三届上海市教育功臣称号 [11]，他还被评为上海市教书育人楷模。
荣誉表彰
时间 | 荣誉/表彰 |
|---|---|
1988年 | 国家有突出贡献中青年专家 |
1989年 | 英国先进技术女皇奖 |
1993年 | 英国先进技术女皇奖 |
2005年 | 感动上海十大人物 |
2006年 | 上海市五一劳动奖章 |
2007年 | 上海市劳动模范 |
2010年4月17日 | 英国约克大学授予荣誉博士学位 |
2013年 | 上海市科技功臣奖 [27] |
2013年 | 上海市教育功臣奖 [27] |
2015年 | 法国棕榈国家教育骑士勋章 [28] |
2016年7月1日 | 全国优秀共产党员 [12] |
上海市优秀共产党员 |
社会任职
播报编辑
时间 | 担任职务 |
|---|---|
中国科学院信息学部常委会副主任 | |
国家可信软件国际联合研究中心主任 | |
教育部可信软件国际合作联合实验室主任 | |
上海市高可信计算重点实验室主任 | |
1996年8月 | 上海交通大学兼职教授、博士生导师 |
1998年8月 | 南京大学兼职教授、博士生导师 |
2003年5月 | |
2006年11月—2011年11月 | 上海市科学技术协会第八届委员会副主席、常务委员、委员 [14] |
2011年11月—2018年9月 | 上海市科学技术协会第九届委员会副主席、常务委员、委员 [15] |
2019年 | 上海市人工智能战略咨询专家委员会委员 [21] |
2019年 | 上海市人工智能产业安全专家咨询委员会主任 [22] |
2019年 | 中国信息技术标准化技术委员会软件与系统工程分技术委员会主任委员 [23] |
人物评价
播报编辑
何积丰是信息领域领军专家，被国际计算机科学界誉为面向模型软件开发方法的奠基石。他在安全软件设计方面的论著被国际软件界广泛引用。他率先提出关系程序设计语言，这项工作被欧洲计算机界认为是继过程语言、函数程序、逻辑程序之后的第四类程序语言的先驱，他因而被欧洲软件界权威人士赞之为“软件设计技术上的一座里程碑”。（中华人民共和国工业和信息化部评）
“何积丰教授在极具应用前景的重要领域中的计算科学方面做出了大量的基础性贡献”。 [18]（图灵奖获得者Hoare 评）
“我发明的关系演算工作主要归功于何积丰的研究”。 [18]（图灵奖获得者Dijkstra 评）
“在过去十五年，何积丰是牛津大学程序研究领域取得成功的驱动力”。 [18]（英国科学技术委员会给政府的报告 评）
“何积丰在软件工程的科学理论与工业实践方面做出了奠基性的工作⋯他发明并开发了计算机系统、通信与标准的精确规范（数学）理论与技术，能以低成本的方式构建高可靠的软件与硬件系统”。 [18]（英国皇家工程院院士McDermid 评）
人物观点
播报编辑
何积丰认为，可信人工智能，主要包含三个要素——人、信息、物理。而所谓的安全，也包括数据安全、技术安全和系统安全。判断是否可信的先决条件之一，是设立关于可信的度量标准。比如，要求数据本身真实可信。数据可信之外是技术可信和系统可信。当人工智能程序或产品发生错误时，对错误或会发生的结果具备可解释性。在其特性或参数发生摄动时，相关系统和技术依旧具备品质指标保持不变的性能，即鲁棒性等。
在他看来，智慧城市和智慧制造已经成为了推动可信AI落地最主要的两大应用场景。智慧城市也就是社会治理的智能化，大数据分析已经在发挥很大的作用。智慧制造方面也在逐步推进。
“从长远来看，我们希望人工智能不是一个简单的工具箱，而是与人类在同一个闭环内相互互动，帮助我们做决策。”何积丰认为，人工智能的发展轨迹可能不是一个线性的变化，而是会迎来指数性的增长机会，“未来或许会有一个爆发性的拐点出现。” [24]
