李未

中国科学院院士、北京航空航天大学前校长男,1943年6月8日出生,北京人,北京航空航天大学前校长,中国科学院院士,计算机专家。
1961年09月—1968年06月,就读于北京大学数学力学系。
1968年06月—1979年07月,先后任北京航空学院基础部、计算中心教师。
1979年07月—1983年01月,在英国爱丁堡大学计算机系攻读博士学位。
1983年01月—1986年08月,任北京航空学院计算机系讲师,
1986年09月任北京航空航天大学计算机学院教授、博士研究生导师。
1997年当选为中国科学院院士。
2002年01月任北京航空航天大学校长,党委副书记。
2009年5月27日,怀进鹏被任命为北京航空航天大学校长,李未院士不再担任北京航空航天大学校长。
学术兼职
国务院学位委员会委员,
国家自然科学基金委员会委员,
国家中长期科技发展规划专家组成员。
软件开发环境国家重点实验室主任,
教育部计算机教学指导委员会主任,
《Frontiers of Computer Science in China》主编,
电子学会副理事长。
英国科学与工程委员会高级研究、
德国不莱梅大学教授级研究员、
德国萨尔布吕肯大学Zuse讲座教授。
第十届全国政协委员
是参与创立、发展和完善结构操作语义方法的主要学者之一,80年代初期,李未院士使用这种方法最先给出了Ada语言有关任务,包括并行、汇聚、通讯、同步及选择等机制的语义,建立了在并行机制下的程序模块以及程序例外处理的语义。他的工作系统地解决了诸如像Ada、Edison等并发式程序设计语言的操作语义问题,并在语义研究的基础上建立了并发语言的翻译与变换理论。
从1992年开始,李未院士根据在863计划实施过程中出现的软件开发方法及知识库的建立和维护等需求,提出了关于形式系统序列、极限及相关的计算模式等一系列的概念和方法,将分析数学中逼近和近似的方法用于软件系统的开发。这一研究在国际上首次提出了以版本作为基本对象、用版本序列描述开发过程、用版本系列极限刻画最终目标的概念和方法。
李未院士用模型的概念和方法,给出了知识库维护过程中“增新扩充”和“出错修正”的合理描述,首次建立了一个“规约修正”演算系统,并给出了基于Prolog语言的“规约修正”算法,该演算系统使程序规约的修正有了可操作的数学方法。他首次提出软件开发策略、知识库维护策略的收敛性概念,并用版本序列的收敛速度衡量维护策略的优劣。在他指导下的课题组成员还研究了力迫、猜想与反驳、归纳等多种软件开发策略,并证明了它们的收敛性。李未院士将这一整套概念和方法称之为“开发逻辑”理论,并曾应邀在德、法、英、丹麦、及瑞典等国的大学就“开发逻辑”理论进行讲演和讲学。
为解决网络环境下拥有海量信息、运行着海量进程的服务软件系统的设计、实现和维护中的重大问题,973“网络环境下海量信息组织与处理的理论与方法研究”项目组从海量信息科学、软件技术与方法以及试验性软件研究三个层次开展了基础研究。两年来,作为该项目的首席科学家,在他的领导下,项目组对此开展了富有成效的研究,取得了丰硕的成果,并顺利通过了科技部主持的项目中期评估,获得重点资助。
在计算机程序语义研究方面,获1995年国家自然科学二等奖。
1999年起,先后担任973计划“网络环境下海量信息的组织与处理的理论与方法研究”和“海量信息的协同性与可生存性的理论和实践研究”项目首席科学家。
提出了修正的演算系统(R-演算),并证明了R-演算的可靠性、完全性和可达性。提出并设计了过程模式语言,提出并研究了合理过程模式的三个基本特性获得1999年光华科技进步一等奖。主持研制的基础设施网络管理系统软件生产平台,获得2004年度国家科技进步二等奖(第一完成人)。
已发表学术论文100余篇,专著1部。获2005年度国家教学成果一等奖,获何梁何利科技进步奖一项。培养博士后8名、博士研究生52名和硕士生96名。