何积丰科研成就科研综述

何积丰科研成就科研综述①创建程序统一理论,奠定了软件语义元理论基础,开创了软件理论的新学派

何积丰与图灵奖获得者Hoare教授创造性地提出了软件的程序统一理论,解决了程序语义的一致性问题,奠定了软件语义元理论基础,开创了程序统一理论学派,出版了英文专著《Unifying Theories of Programming》,该文献他引超过800次

程序统一理论已被国际上公认为研究各类程序语言的一种标准方法

自2006年起,每两年举办一次程序统一理论国际学术研讨会,包括牛津大学、约克大学、巴黎11大等在内的世界著名研究机构从事序统一理论的相关研究

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

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

该成果被国际计算机科学界誉为“面向模型软件开发的一个里程碑”

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

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

 二零一七年香山科学会议,何积丰在世界上首次提出“可信人工智能”,自此世界各地开始广泛关注人工智能的安全可信问题

 学术论著截至2018年,何积丰出版英文专著2部,在国际期刊和会议上发表论文160余篇,他引4000余次 

He Jifeng and C.A.R. Hoare. "Algebraic specification and proof of a distributed recovery algorithm" Distributed Computing Vol 2, 1-12, (1987) 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) He Jifeng. "Hybrid Parallel Programming and Implementation of Synchronised Communication" Lecture Notes of Computer Science 711, 537-547, Springer, (1993) He Jifeng. "A Predicative Semantics for the Refinement of Real-time Systems" Lecture Notes of Computer Science 802, 230-249, Springer, (1994) He Jifeng and C.A.R. Hoare. “Linking theories in probabilistic programming” Information Sciences, vol 119, 205-218, (1999) He Jifeng "An Algebraic Approach to Verilog Programming" Lecture Notes in Computer Science 2757, 65-81, (2002) 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) He Jifeng "Linking theories of concurrency" (Invited talk) In Proceedings of CSP'25, Springer, (2004) Jifeng He, Jeff W. Sanders: Unifying Probability. UTP 2006: 173-199 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 承担项目截至2020年,何积丰先后担任国家自然科学基金委重大研究计划、科技部973计划、863计划主题项目首席科学家,领衔国家自然科学基金委创新研究群体 

时间项目名称项目来源2001年—2003年VERILOG仿真器和合成器设计上海市信息委项目(CX20010005)2002年—2004年UML软件开发进程的形式化理论教育部重点项目(02104)2002年—2007年网构软件形式化理论与方法研究国家科技部973项目(2002CB31200001)2003年—2005年安全软件理论与软硬件协同设计“211”项目2007年-2010年海量信息的协同性和可生存性的理论与实践国家科技部973计划 2007年可信软件基础研究国家自然科学基金委员会 2007年计划信息物理融合系统主题项目国家科技部863计划 2017年-2019年工业互联网,物联网安全操作系统产业化及规模化应用国家工信部 2020年-2023年人工智能安全可信理论及验证平台科技创新2030 科研成果奖励截至2020年,何积丰先后以唯一完成人获得国家自然科学奖二等奖和上海市科技进步奖一等奖各1项,以项目第一完成人荣获上海市科技进步奖特等奖 ,以第一完成人获省部级科技进步奖与科技成果奖一等奖4项 

时间项目名称奖励名称1985年电子工业部软件一等奖1986年上海市科技进步一等奖2000年设计严格安全软件的完备演算系统上海市科技进步一等奖 2002年设计严格安全软件的完备演算系统国家自然科学二等奖 2012年基于模型的可信软件理论与开发方法教育部高等学校科学研究成果奖(自然科学)一等奖 2013年-何梁何利基金科学与技术进步奖 2014年高端软件人才的协同创新培养模式高等教育上海市教学成果奖特等奖 2017年面向综合能力提升的卓越软件人才培养体系上海市教学成果奖一等奖 2018年逻辑思维与工具实践并重的跨领域可信软件人才培养模式 国家级教学成果奖二等奖 2020年面向重大工业装备核心控制软件的安全可信保障技术及应用上海市科技进步特等奖 

以上内容由大学时代综合整理自互联网,实际情况请以官方资料为准。

相关