何积丰于1943年8月5日出生在上海市,是计算机软件专家,中国科学院院士,上海华科智谷人工智能研究院院长,原华东师范大学软件学院院长、教授、博士生导师。[2]
1965年,何积丰从复旦大学数学系毕业,并被分配至华东师范大学工作;1972年,何积丰参与华东师范大学国产计算机研制项目。1980年,他被派往美国旧金山大学进修。1984年至1998年,何积丰任英国牛津大学客座教授、高级研究员;1998年至2005年,他任澳门联合国大学国际软件技术研究所研究员。2002年,他成为华东师范大学首批终身教授;2009年,他被聘为杭州师范大学杭州国际服务工程学院院长;2010年,他被英国约克大学授予荣誉博士学位。2014年,何积丰受聘成为上海农业物联网首席专家;2016年,他被聘为华东师范大学计算机科学与软件工程学院院长。2019年,何积丰又被聘为同济大学特聘教授,并入职同济大学交通运输工程学院。[2][4][5][6]
何积丰担任中国国家自然科学基金委可信软件基础重大研究计划、科技部973计划海量信息处理项目以及863计划信息物理融合系统主题项目首席科学家。出版英文专著2部,在国际期刊和会议上发表论文160余篇,他引4000余次。担任多个国际著名学术会议主席、国际权威学术期刊编委。他以唯一完成人获国家自然科学二等奖和上海市科技进步一等奖各1项,以第一完成人获省部级科技进步奖与科技成果奖一等奖4项,两次荣获英国女王先进技术奖,于2013年获得何梁何利基金科学与技术进步奖和上海市科技功臣称号。[7]
早年经历
何积丰于1943年8月5日出生于上海市,高中毕业后考入复旦大学数学系,1965年2月毕业于复旦大学数学系。[2][4][5]
工作经历
1965年3月,何积丰任职于华东师范大学,从事教学、科研和管理工作。1972年,上海市要求复旦大学、华东师范大学研制国产计算机。何积丰参与华东师范大学国产计算机研制项目,负责计算机的运算控制部分,两年多后计算机研制成功。[4][5]
1980年7月至1981年7月,何积丰作为访问学者被华东师范大学派往美国旧金山大学进修计算机应用,并在斯坦福大学学习。1984年12月,何积丰在英国牛津大学计算机实验室任客座教授、高级研究员(至1998年7月)。1986年,何积丰与C.A.R.Hoare提出了“程序分解算子”,并将规范语言与程序语言看成是同一类数学对象,还提出采用“关系代数”作为程序和软件规范的统一数学模型,在数据精化方面给出了处理非确定性程序语言数据精化的完备方法。同年8月何积丰晋升为华东师范大学教授。[6][8]
1995年,何积丰与C.A.R.Hoare提出了程序设计统一理论和连接各类程序理论的数学法则,还提出用形式化的界面理论沟通几种程序语言,以及非确定性数据流的数学模型及代数定律。同年8月何积丰被聘为华东师范大学博士生导师。[6][8]1998年7月,何积丰任联合国大学国际软件技术研究所高级研究员(至2005年)。[4][6]

2001年11月,何积丰担任华东师范大学软件学院院长。2002年12月,何积丰成为华东师范大学首批终身教授。2005年,何积丰当选中国科学院院士。2008年5月,何积丰担任天津师范大学软件学院名誉院长。2009年,何积丰受聘为杭州师范大学杭州国际服务工程学院院长。2010年,何积丰被英国约克大学授予荣誉博士学位。2014年10月22日,何积丰受聘为上海农业物联网首席专家。2016年,何积丰受聘为华东师范大学计算机科学与软件工程学院院长。[4][6]2019年,何积丰受聘为同济大学特聘教授,入职同济大学交通运输工程学院。[2]
研究方向
何积丰的主要研究领域:高可信与信息安全理论、形式化方法、并发程序设计理论、嵌入式系统设计方法和工具、软硬件混成系统协同设计、计算机软件与理论。[9]何积丰长期从事计算机软件理论及其应用研究,针对软件的复杂性、正确性和可靠性等问题开展了系统性的研究。完整地揭示了软件的本质,彻底解决了程序语义的一致性问题;创新了软件开发方法学,有效地降低了测试成本;解决了在开放环境如何保障软件正常工作等科学问题,推动了可信嵌入式软件行业的发展。他是程序统一理论(Unifying Theories of Programming,简称UTP)的创立者、数据精化完备理论的奠基者、可信软件设计理论与技术的开拓者。[10]
发表论文
| 时间 | 成果 |
|---|---|
| 2018年 | 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 |
| 2007年 | He Jifeng: Linking Semantic Models. ICTAC 2007: 18-33 |
| He Jifeng: UTP Semantics for Web Services. IFM 2007: 353-372 | |
| He Jifeng‚Zhu Huibiao‚Pu Geguang: A model for BPEL-like languages‚Front.Comput.Sci.China 2007‚1(1):9-19 | |
| Jifeng He: Compensable Programs. Formal Methods and Hybrid Real-Time Systems 2007: 349-363 | |
| 2006 | Jifeng He‚ Jeff W. Sanders: Unifying Probability. UTP 2006: 173-199 |
| Jifeng He‚ C. A. R. Hoare: CSP Is a Retract of CCS. UTP 2006: 38-62 | |
| Jifeng He‚ Shengchao Qin‚ Adnan Sherif: Constructing Property-Oriented Models for Verification. UTP 2006: 85-100 | |
| Jifeng He‚ Xiaoshan Li‚ Zhiming Liu: A Theory of Reactive Components. Electr. Notes Theor. Comput. Sci. 160: 173-195 (2006) | |
| Jifeng He‚ Xiaoshan Li‚ Zhiming Liu: rCOS: A refinement calculus of object systems. Theor. Comput. Sci. 365(1-2): 109-142 (2006) | |
| 2005年 | Jifeng He: Linking Theories of Concurrency by Retraction. ICDCIT 2005: 432 |
| Jifeng He‚ C. A. R. Hoare: Linking Theories of Concurrency. ICTAC 2005: 303-317 | |
| Jifeng He‚ Xiaoshan Li‚ Zhiming Liu: Component-Based Software Engineering. ICTAC 2005: 70-95 | |
| Jifeng He‚ Dang Van Hung‚ Geguang Pu‚ Zongyan Qiu‚ Wang Yi: Exploring optimal solution to hardware/software partitioning for synchronous model. Formal Asp. Comput. 17(4): 443-460 (2005) | |
| 2004年 | Jifeng He: Linking Theories of Concurrency. 25 Years Communicating Sequential Processes 2004: 61-74 |
| Jifeng He‚ Zhiming Liu‚ Xiaoshan Li‚ Shengchao Qin: A Relational Model for Object-Oriented Designs. APLAS 2004: 415-436 | |
| Jifeng He‚ Carroll Morgan‚ Annabelle McIver: Deriving Probabilistic Semantics Via the ´Weakest Completion´. ICFEM 2004: 131-145 | |
| Jifeng He‚ Naiyong Jin: Integrating Variants of DC. ICTAC 2004: 14-34 | |
| 2003年 | 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) |
| 2002年 | He Jifeng "An Algebraic Approach to Verilog Programming" Lecture Notes in Computer Science 2757, 65-81, (2002) |
| 1999年 | He Jifeng and C.A.R. Hoare. “Linking theories in probabilistic programming” Information Sciences, vol 119, 205-218, (1999) |
| 1994年 | He Jifeng. "A Predicative Semantics for the Refinement of Real-time Systems" Lecture Notes of Computer Science 802, 230-249, Springer, (1994) |
| 1993年 | He Jifeng. "Hybrid Parallel Programming and Implementation of Synchronised Communication" Lecture Notes of Computer Science 711, 537-547, Springer, (1993) |
| 1990年 | 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) |
| 1987年 | He Jifeng and C.A.R. Hoare. "Algebraic specification and proof of a distributed recovery algorithm" Distributed Computing Vol 2, 1-12, (1987) |
参考资料[1][9][11][12][13][14][15][16][17]
发表文章
| 文章名称 | 期刊 | 出版期数 |
|---|---|---|
| 《传承40年深厚积累 共同开启软件工程标准化新篇章》 | 信息技术与标准化 | 2024 第C1期 |
| 《面向城轨云平台边界安全防护的动态信任管理方法》 | 同济大学学报(自然科学版) | 2024 第52卷 第2期 |
| 《面向冲突化解的双线交汇区段列车编队双层优化模型》 | 同济大学学报(自然科学版) | 2024 第52卷 第1期 |
| 《隐私计算的关键理论与前沿应用》 | 中国科学基金 | 2024 第38卷 第4期 |
| 《基于SMT的区域控制器同步反应式模型的形式化验证》 | 软件学报 | 2023 第34卷 第7期 |
| 《可信机器学习的公平性综述》 | 软件学报 | 2021 第32卷 第5期 |
| 《智能制造与安全可信人工智能》 | 信息安全与通信保密 | 2020 第12期 |
| 《安全可信人工智能》 | 信息安全与通信保密 | 2019 第10期 |
| 《重视人工智能发展中的安全与治理》 | 信息安全与通信保密 | 2019 第6期 |
| 《基础学科教学的智能化》 | 科学中国人 | 2019 第17期 |
| 《人工智能为工控安全护驾》 | 信息安全与通信保密 | 2018 第10期 |
| 《工业APP是推动工业互联网的重要手段》 | 中国信息化周报 | 2019 第20期 |
| 《人工智能与安全——人工智能为工控安全护驾》 | 信息安全与通信保密 | 2018 第10期 |
| 《“可信软件基础研究”重大研究计划结题综述》 | 中国科学基金 2018 | 第32卷 第3期 |
以上为部分文章,参考资料来自[18]
出版书籍
| 书籍名称 | 出版社 | 初版日期 |
|---|---|---|
| 《高校计算机教学与研究 第3辑》[3] | 北京:科学出版社 | 2010 |
主要成就
何积丰担任中国国家自然科学基金委可信软件基础重大研究计划、科技部973计划海量信息处理项目以及863计划信息物理融合系统主题项目首席科学家,领衔国家自然科学基金委创新研究群体。出版英文专著2部,在国际期刊和会议上发表论文160余篇,他引4000余次。担任多个国际著名学术会议主席、国际权威学术期刊编委。他以唯一完成人获国家自然科学二等奖和上海市科技进步一等奖各1项,以第一完成人获省部级科技进步奖与科技成果奖一等奖4项,两次荣获英国女王先进技术奖,于2013年获得何梁何利基金科学与技术进步奖和上海市科技功臣称号。[7]
创建程序统一理论
创建程序统一理论,奠定了软件语义元理论基础,开创了软件理论的新学派。何积丰与图灵奖获得者Hoare教授创造性地提出了软件的程序统一理论,解决了程序语义的一致性问题,奠定了软件语义元理论基础,开创了程序统一理论学派,出版了英文专著《Unifying Theories of Programming》,该文献他引超过800次。程序统一理论已被国际上公认为研究各类程序语言的一种标准方法。自2006年起,每两年举办一次程序统一理论国际学术研讨会,包括牛津大学、约克大学、巴黎11大等在内的世界著名研究机构从事序统一理论的相关研究。[10]
创新软件开发方法学
创新软件开发方法学,建立了数据精化完备理论,被国际上誉为“面向模型软件开发的一个里程碑”。针对软件开发各阶段模型正确性问题,何积丰创建了数据精化完备理论,首次提出了数据精化的“程序分解算子”与“上下仿真映照对”方法,将规范语言与程序语言看成是同一类数学对象,采用“关系代数”作为程序和软件规范的统一数学模型,在此框架中建立了求解规范方程的演算法则。该成果被国际计算机科学界誉为“面向模型软件开发的一个里程碑”。[10]
数据精化完备理论被多种主流软件开发方法所采用,如B软件开发方法与Z软件开发方法。其中,B软件开发方法已成为法国商业工具Atelier B的核心技术,被法国阿尔斯通、德国西门子等公司成功地应用于严格轨道交通软件的开发。[10]
开拓可信嵌入式软件设计理论与技术
开拓可信嵌入式软件设计理论与技术,促进了方法与技术在安全攸关行业领域的应用。何积丰创造性地开拓和发展了基于模型的可信软件开发与验证研究领域,建立了正确性系统的可证理论与方法,解决了可信嵌入式系统构造与验证技术的若干关键问题,并应用于轨道交通、汽车电子、航天控制等安全攸关行业,推动了相关产业发展。[10]
学术成果
2020年5月,依托同济大学领衔的“智能科学与技术”上海市高峰学科,创建“可信人工智能研究所”,聚焦可信人工智能基础理论、共性技术与算法应用,特别是针对人工智能系统与算法的可信安全关键问题,研究人工智能与机器学习的鲁棒性、不确定性、可解释性、公平性等关键理论,研究多智能体协同智能算法与系统关键技术,研究可信智能算法、软件、芯片以及分布式联邦可信计算平台,研究以智能网联车为落地场景的可信人工智能技术应用,推进人工智能在智慧交通、智慧医疗、金融科技等领域的应用,促进基础研究与创新创业深度融合,助力最新智能技术的成果转化。[19]
社会活动
2010年10月28日,何积丰参加了在无锡召开的2010中国国际物联网(传感网)大会,并在大会上做了主题为“物联网中的若干问题”的演讲。[20]
2017年,在S36次香山科学会议中,何积丰在世界范围内首次提出可信人工智能的概念。[21]
2020年8月,何积丰参加了在中以(上海)创新园举行的普陀区科技节启动仪式。[22]
2022年11月21日,在2022(第16届)创业周暨全球创业周中国站闭幕式上,何积丰发表了主题《可信人工智能的展望》的演讲。[23]
2023年10月11-12日,第十一届上海院士专家峰会暨大飞机创新谷生态大会在中国商飞上海飞机设计研究院举行。何积丰作了主题为《人工智能时代安全攸关系统软件开发方法展望》的报告,提到人工智能技术在安全攸关产业的应用、相关挑战和解决方案,以及C919上人工智能技术的一些应用场景,并表示希望与中国商飞合作推动大飞机产业高质量发展。[24]

2024年9月,何积丰参加了20日至22日在山西太原举行了主题为“万物互联 晋善晋美”第十八届中国物联网(传感器网络)学术会议(CWSN 2024),并做特邀报告。[25]
2024年11月,何积丰在2024Bilibili超级科学晚活动上发表主题为《普通人如何使用AI大模型》的演讲。何积丰表示,自1956年提出AI概念以来,AI技术迎来了AI第一段发展期——反思发展期——第二次发展高潮——AlphaGo引发全民AI热潮阶段。[2]

社会任职
何积丰担任多个国际著名学术会议主席、国际权威学术期刊编委。[10]
2006年11月-2018年9月,何积丰担任上海市科学技术协会第八届和第九届委员会副主席、常务委员、委员。[26][27]
2019年4月,何积丰担任全国信息技术标准化技术委员会第三届软件与系统工程分技术委员会主任委员,[28]同年何积丰担任上海人工智能安全专委会主任、上海市人工智能战略咨询专家委员会委员。[29][30]
教育理念
2001年,何积丰响应党和国家号召,受命组建国家首批示范性软件学院之一的华东师范大学软件学院。在他的带领下,软件学院从成立时的5人发展到百余人的规模,向社会输送3000多名“本硕博”专业人才,创设教育部软硬件协同设计技术与应用工程研究中心、上海市高可信计算实验室以及多个国家级和省部级重点研究基地,2010年入选国家基金委“创新研究群体”,是上海高校在计算机领域获“创新研究群体”资助的唯一一家。2015年扩展为计算机科学与软件工程学院,成为中国高校计算机软件工程领域的领军团队。软件工程学科经教育部评估全国排名第四,列入上海市一流学科建设。[31]
何积丰率先提出卓越软件人才的协同创新培养模式,先后与中国外高校及中国电科集团第32所、Intel等企事业单位成立了多个合作研究实验室,并与微软等名企合作共建了10余门课程,以多元协作的方式,全面培养软件行业人才的综合创新能力。何积丰坚持国际化办学,非常重视本科教学改革,全面推进双语和全英文课程建设,引进国外课程、采用原版教材、试行教考分离、实行月考制度,将专业课程设置与工业界实际需求接轨,改变学业评价方式,从单一考试拓展为以考试、研究项目、学术论文进行综合评价,要求专职老师从事学生实践项目管理,学生提早进老师实验室。[31]
主讲课程
何积丰为本科生开设了第一门由院士主讲的通识教育课程——计算机文化,并梳理了自己多年的科研成果,为研究生开设了《程序统一理论》课程。[32]
家庭情况
1980年,何积丰被华东师范大学派到美国旧金山大学进修,他的妻子张蕾蕾全力支持他,一个人抚养着刚出生不久的女儿。然而,在何积丰去美国后半年,张蕾蕾在一起意外事故中受伤,双目失明。为了不影响丈夫的学业和事业,她向何积丰隐瞒了真相。一年的美国进修结束后,何积丰带妻子看医生,然而重见光明的希望没有实现。为了不成为丈夫的累赘,张蕾蕾向丈夫提出离婚,何积丰没有答应,三十余年如一日地做妻子的“眼睛”。[33]
个人习惯
何积丰养生是轻微运动,每天散步,还注意控制饮食,不吸烟、不喝酒,只喝白开水。[33]
人物观点
何积丰认为,大模型的安全问题主要是在未经同意的情况下,收集、使用和泄露个人信息。隐私问题既可能发生在训练过程,也可能发生在使用过程中,而大模型的生成能力则让“隐私泄露”的方式变得多样化,造成隐私保护更加困难。[34]
何积丰介绍,反馈强化学习是实现对齐的技术途径,目前有两种方式,一种方式是通过人工反馈给模型不同的奖励信号,引导模型的高质量输出;另一种方式,事先给大模型提供明确的原则,系统自动训练模型对所有生成的输出结果提供初始排序。“这意味着,不仅智能系统需要向人类价值观对齐,人类的训练方法也要向价值观对齐。”何积丰说。[34]
何积丰称,大模型时代的隐私问题跟传统的机器学习是有差别的,一是大模型在训练过程中,涉及大量用户个人信息和数据;二是使用过程中涉及很多用户私密信息,这些信息没有受到应有的隐私保护,用户在使用时面临“要么失去隐私、要么失去服务”的选择;三是大模型的生成能力让隐私泄露变得更加容易也更加多样化,隐私保护变得更加困难。[2]
何积丰指出,AI 就像孙悟空,需要唐僧的紧箍咒保证其不任意使用他的能力去闯祸、胡作非为,对齐就是控制 AI 安全的核心技术,对齐是指系统的目标和人类价值观一致,使其符合设计者的利益和预期,不会产生意外的有害后果。何积丰以机器人为例,机器人学的第一定律就是不得伤害人类或因不作为使人类受到伤害。[2]
何积丰强调,在 AI 发展过程中,千万不要忘记人类的核心角色,“AI技术是我们的助手,而不是代替人类创造新世界的未来。”[2]
“我们应该以开放的心态拥抱变化,相信AI技术会给我们带来更加美好的未来。”何积丰称。[2]
人物评价
何积丰教授在极具应用前景的重要领域中的计算科学方面做出了大量的基础性贡献。(图灵奖获得者Hoare评)[9]
我发明的关系演算工作主要归功于何积丰的研究。(图灵奖获得者Dijkstra评)[9]
在过去十五年,何积丰是牛津大学程序研究领域取得成功的驱动力。(英国科学技术委员会给政府的报告评)[9]
何积丰在软件工程的科学理论与工业实践方面做出了奠基性的工作⋯他发明并开发了计算机系统、通信与标准的精确规范(数学)理论与技术,能以低成本的方式构建高可靠的软件与硬件系统。(英国皇家工程院院士McDermid评)[9]
何教授对党委工作要求特别高,他经常说,要充分发挥党支部的战斗堡垒作用,每一位党员都应该在自己的本职岗位上发挥先锋模范带头作用。(华东师大计算机科学与软件工程学院党委书记李恺评)[38]
何老师始终把学术事业和祖国的命运与党领导的事业密切地联系在一起,为自己能够在国家发展、学术发展和整个社会的进步中发挥作用而感到自豪。(华东师范大学党委书记童世骏评)[38]
党龄33年、育人51载,何积丰始终坚守在教学和科研的第一线。他胸怀党和国家事业,带领团队培养了数千名高层次软件人才;他攻关科研、开拓创新,秉持执着追求的科学精神,开创可信软件研究新领域;他敢于担当、积极作为,取得了丰硕的教学科研成果,成为我国信息领域领军专家,践行了一名共产党员的誓言。(光明日报评)[39]
当了51年教师,何积丰高度注重青年教师与青年学子道德品性的塑造,每当有青年教师入职,他都会与其沟通交流、一起制定发展规划。他大胆向学校提出人才计划体制改革的设想,为青年教师设立专门的帮扶基金,创造宽松、良好、和谐的工作环境。(人民日报评)[40]
何积丰与英国计算机科学家、图灵奖获得者托尼·霍尔一起创造性地提出了软件领域的程序统一理论,开创了程序统一理论的国际学派,奠定了软件语义元理论基础;他建立了数据精化的完备理论,被国际计算机科学界誉为“面向模型软件开发的一个里程碑”;他系统性地构建了基于模型的可信软件设计方法与开发技术,被称赞为在软件工程的科学理论与工业实践方面“做了奠基性的工作。(人民日报评)[40]
获得荣誉
参考资料[10][8][7][35][36][37][32]
参考资料 40
- A new roadmap for linking theories of programming and its applications on GCL and CSP — sciencedirect
- 中国科学院院士何积丰:普通人如何用好AI大模型产生更大价值 — 腾讯网
- 参考 3
- 何积丰 — 杭州电子科技大学计算机学院
- 媒体关注|何积丰:一位院士的三次选择 — 华东师范大学
- 何积丰 — 科创中国
- 实验室主任 — 华东师范大学高可信计算重点实验室
- 何积丰院士 — 同济大学交通运输工程学院
- 何积丰 — 华东师范大学教师个人主页
- 何积丰 — 华东师范大学高可信计算重点实验室
- Advanced Features of Duration Calculus and Their Applications in Sequential Hybrid Programs — springer
- An Algebraic Approach to the VERILOG Programming — springer
- Linking theories in probabilistic programming — sciencedirect
- A Predicative Semantics for the Refinement of Real-Time Systems — acm
- Hybrid parallel programming and implementation of synchronised communication — springer
- Categorical semantics for programming languages — springer.
- Algebraic specification and proof of a distributed recovery algorithm — springer
- 参考 18
- 董德存教授课题组 — 同济大学交通运输工程学院 综合交通信息与控制工程系
- 中国科学院院士何积丰做主题演讲 — 网易
- 专访何积丰院士:达成可信的人工智能,最重要的支点在人 — 人民资讯
- 科普云游、互动游戏……普陀区科技节盛大开启 — 上海市科学技术协会
- 数十场行业专场路演云端见 — 上海市科学技术协会
- 汇聚创领智力 共话蓝天科技 第十一届上海院士专家峰会暨大飞机创新谷生态大会顺利举行 — 上海市科学技术协会
- 何积丰、张宏科、吕建、崔铁军4位院士邀你共话万物互联|CWSN2024 — 中国计算机学会
- 第八届委员会(2006.11- 2011.11 ) — 上海市科学技术协会
- 第九届委员会(2011.11-2018.9) — 上海市科学技术协会
- 关于全国信息技术标准化技术委员会第三届软件与系统工程分技术委员会换届及组成方案进行公示的通知 — 中国国家标准化管理委员会
- 上海人工智能发展“智囊团”再添大咖,李强为他们颁发聘书 — 澎湃新闻
- 上海市人工智能产业安全专家咨询委员会成立 发起《人工智能安全发展上海倡议》 — 新民晚报
- 优秀党员展风采|何积丰:厚积喜获丰收 大爱成就梦想 — 华东师范大学
- 何积丰先进事迹 — 人民网
- 程序开拓者何积丰:与盲妻41年爱情感天动地 — 东方早报
- 外滩大会|何积丰院士:保护隐私安全,大模型“对齐”有哪些挑战? — 澎湃新闻
- 科研获奖 — 华东师范大学软件工程学院
- 参考 36
- 参考 37
- 不断积累的人生才丰硕 — 光明网
- 何积丰:大爱铸就科技梦想 — 光明网
- 中国科学院院士、华东师范大学终身教授何积丰:“积”成“丰”收 圆软件中国梦 — 人民网