何积丰，著名计算机软件科学家。1943年8月5日生于上海，1965年毕业于复旦大学。2005年当选为中国科学院院士。2010年被英国约克大学授予荣誉博士学位。现为华东师范大学终身教授、软件学院院长，中国科学院信息学部常委会副主任，上海市科协副主席，国家可信嵌入式软件工程技术研究中心首席科学家，上海市高可信计算重点实验室主任，上海高校知识服务平台可信物联网产学研联合研发中心主任。

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

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

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

程序统一理论被应用于多个计算机领域：在软件顶层设计领域，该理论被用于规范语言的设计与面向对象分析，如基于UTP的面向对象分析语言rCOS及其支撑工具成功地应用在大规模程序分析中；在软硬件构建领域，该理论被应用于编译器构造与芯片正确性证明，如基于UTP的证明技术发现了英国著名芯片公司Transputer芯片的三个错误；在产品验证领域，该理论被应用于自动测试与定理证明器的开发，如基于UTP的定理证明器被成功地应用于嵌入式软件产品的形式化验证。

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

针对软件开发各阶段模型正确性问题，何积丰创建了数据精化完备理论，首次提出了数据精化的“程序分解算子”与“上下仿真映照对”方法，将规范语言与程序语言看成是同一类数学对象，采用“关系代数”作为程序和软件规范的统一数学模型，在此框架中建立了求解规范方程的演算法则。该成果被国际计算机科学界誉为“面向模型软件开发的一个里程碑”。

数据精化完备理论被多种主流软件开发方法所采用，如B软件开发方法与Z软件开发方法。其中，B软件开发方法已成为法国商业工具Atelier B的核心技术，被法国阿尔斯通、德国西门子等公司成功地应用于严格轨道交通软件的开发。

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

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

在轨道交通领域，研发的模型驱动的可信软件开发工具，应用于上海贝尔阿尔卡特公司的车载信号软件的分析与验证，提高了车载信号系统模块的可靠性；在汽车电子领域，研发的形式化验证工具链，对上海普华开发的国产汽车电子操作系统进行了验证，成为我国第一个经过形式化验证的汽车操作系统，验证后的操作系统成功地通过了欧洲OSEK标准化组织的认证，并第一次出口欧洲；在航天领域，研发的嵌入式系统需求分析技术，应用于航天五院重要型号的软件开发过程，该技术改变了航天软件需求依靠人工分析的现状，型号办公室评价该技术“为保障型号任务的顺利完成做出了主要贡献”。

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

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

何积丰敢为天下先、潜心治学 ，以温润的情怀教书育人。他胸怀“以学生为本、服务社会”的教育理念，践行人才协同创新培养，创建和发展华东师大软件学院，培养行业专门人才3000余名。曾获上海市教书育人楷模、上海高校教学名师、上海市五一劳动奖章、上海市优秀共产党员、上海市劳动模范等称号。