何积丰，男，中国科学院院士，著名计算机软件科学家，英国约克大学荣誉博士。现为华东师范大学终身教授、软件学院院长，中国科学院信息学部常委会副主任，上海市科协副主席，国家可信嵌入式软件工程技术研究中心首席科学家，上海市高可信计算重点实验室主任，上海高校知识服务平台可信物联网产学研联合研发中心主任。

何积丰长期从事计算机软件理论及其应用研究，针对软件的复杂性、正确性和可靠性等问题开展了系统性的研究。完整地揭示了软件的本质，彻底解决了程序语义的一致性问题；创新了软件开发方法学，有效地降低了测试成本；解决了在开放环境如何保障软件正常工作等科学问题，推动了可信嵌入式软件行业的发展。他是程序统一理论（Unifying Theories of Programming，简称UTP）的创立者、数据精化完备理论的奠基者、可信软件设计理论与技术的开拓者。主要科学贡献：

（1）创建程序统一理论，奠定了软件语义元理论基础，开创了软件理论的新学派。

何积丰与图灵奖获得者Hoare教授创造性地提出了软件的程序统一理论，解决了程序语义的一致性问题，奠定了软件语义元理论基础，开创了程序统一理论学派，出版了英文专著《Unifying Theories of Programming》，该文献他引超过800次。程序统一理论已被国际上公认为研究各类程序语言的一种标准方法。自2006年起，每两年举办一次程序统一理论国际学术研讨会，包括牛津大学、约克大学、巴黎11大等在内的世界著名研究机构从事程序统一理论的相关研究。

（2）创新软件开发方法学，建立了数据精化完备理论，被国际上誉为“面向模型软件开发的一个里程碑”。

针对软件开发各阶段模型正确性问题，何积丰创建了数据精化完备理论，首次提出了数据精化的“程序分解算子”与“上下仿真映照对”方法，将规范语言与程序语言看成是同一类数学对象，采用“关系代数”作为程序和软件规范的统一数学模型，在此框架中建立了求解规范方程的演算法则。该成果被国际计算机科学界誉为“面向模型软件开发的一个里程碑”。数据精化完备理论被多种主流软件开发方法所采用，如B软件开发方法与Z软件开发方法。其中，B软件开发方法已成为法国商业工具Atelier B的核心技术，被法国阿尔斯通、德国西门子等公司成功地应用于严格轨道交通软件的开发。

（3）开拓可信嵌入式软件设计理论与技术，促进了方法与技术在安全攸关行业领域的应用。

何积丰创造性地开拓和发展了基于模型的可信软件开发与验证研究领域，建立了正确性系统的可证理论与方法，解决了可信嵌入式系统构造与验证技术的若干关键问题，并应用于轨道交通、汽车电子、航天控制等安全攸关行业，推动了相关产业发展。

何积丰担任国家自然科学基金委可信软件基础重大研究计划、科技部973计划海量信息处理项目以及863计划信息物理融合系统主题项目首席科学家，领衔国家自然科学基金委创新研究群体。出版英文专著2部，在国际期刊和会议上发表论文160余篇，他引4000余次。担任多个国际著名学术会议主席、国际权威学术期刊编委。他以唯一完成人获国家自然科学二等奖和上海市科技进步一等奖各1项，以第一完成人获省部级科技进步奖与科技成果奖一等奖4项，两次荣获英国女王先进技术奖，于2013年获得何梁何利基金科学与技术进步奖和上海市科技功臣称号。

何积丰所取得的科学贡献在国内外产生了重要影响。图灵奖获得者Hoare 评价“何积丰教授在极具应用前景的重要领域中的计算科学方面做出了大量的基础性贡献”。图灵奖获得者Dijkstra评价“我发明的关系演算工作主要归功于何积丰的研究”。1998年英国科学技术委员会给政府的报告中对何积丰给予高度评价“在过去十五年，何积丰是牛津大学程序研究领域取得成功的驱动力”。2010年，何积丰荣获英国约克大学荣誉博士学位，英国皇家工程院院士McDermid在授予仪式上赞誉“何积丰在软件工程的科学理论与工业实践方面做出了奠基性的工作⋯他发明并开发了计算机系统、通信与标准的精确规范（数学）理论与技术，能以低成本的方式构建高可靠的软件与硬件系统”。

何积丰敢为天下先、潜心治学 ，以温润的情怀教书育人。他胸怀“以学生为本、服务社会”的教育理念，践行人才协同创新培养，创建和发展华东师大软件学院，培养行业专门人才3000余名。曾获上海市教书育人楷模、上海高校教学名师、上海市五一劳动奖章、上海市优秀共产党员、上海市劳动模范等称号，并于2013年获得上海市教育功臣称号。2015年12月获法国国家棕榈教育骑士勋章、2016年7月1日在北京人民大会堂出席建党95周年庆祝大会并获“全国优秀共产党员”称号。