软件所形式化 林惠民 院士
报告生成时间：2026年8月20日
个人主页：林惠民
所属团队：中国科学院软件研究所 / 计算机科学国家重点实验室
一、学者基本信息
| 项目 | 内容 |
|---|---|
| 姓名 | 林惠民 |
| 性别 | 男 |
| 出生日期 | 1947年11月 |
| 出生地 | 福建省福州市 |
| 国籍 | 中国 |
| 职称 | 中国科学院院士、研究员、博士生导师 |
| 工作单位 | 中国科学院软件研究所 |
| 所属实验室 | 计算机科学国家重点实验室（曾任主任，现任学术委员会主任） |
| 电子邮件 | lhm@ios.ac.cn |
| 通信地址 | 北京市海淀区中关村南四街4号中国科学院软件研究所（100190） |
| 研究领域 | 并发理论、形式化方法、进程代数、模型检测、π-演算 |
| 招生专业 | 081202-计算机软件与理论 |
| 招生方向 | 网络与并发实时系统的设计与分析、并发理论与模型检测、形式化方法 |
二、教育背景与职业履历
林惠民1947年出生于福建省福州市。少年时期在福州第三中学就读期间曾两次在市级数学竞赛中获奖。1966年高中毕业时恰逢"文化大革命"，高考取消，他于1969年到闽北山区建宁县插队务农。1972年回城后进入福州八一磷肥厂当工人，先后在多个车间从事重体力劳动，后正式分配至机修车间担任铣工。1975年在工厂开办的"七二一"工人大学负责教数学。
1977年恢复高考后，林惠民报考福州大学数学系，1978年初被录取至福州大学计算机系软件专业。他的求学历程体现了鲜明的时代特征和个人奋斗精神：
- 1978年2月—1982年2月：就读于福州大学计算机系，获计算机软件专业学士学位。
- 1982年2月—1986年6月：就读于中国科学院软件研究所，获计算机科学理论专业博士学位。博士毕业后留所工作。
- 1986年9月—1987年12月：赴英国爱丁堡大学计算机科学基础实验室从事博士后研究（Research Fellow）。爱丁堡大学是进程代数创始人Robin Milner的工作所在地，这段经历对林惠民后来的研究方向产生了深远影响。
- 1988年1月—1990年3月：任中国科学院软件研究所副研究员。
- 1990年4月—1993年3月：任英国萨塞克斯大学（University of Sussex）Research Fellow。
- 1993年：晋升为中国科学院软件研究所研究员。
- 1994年：被聘为博士生导师。
- 1999年11月：当选为中国科学院院士，同年担任计算机科学国家重点实验室主任。
林惠民自1986年留所工作至今，长期在中国科学院软件研究所从事研究工作，是中国形式化方法领域的主要开创者和领军人物之一。软件研究所计算机科学国家重点实验室先后涌现了唐稚松、董蕴美、周巢尘、林惠民四位中科院院士，是中国形式化方法研究的核心基地。
三、学生培养情况
林惠民作为博士生导师，长期在中国科学院大学招收计算机软件与理论专业的博士和硕士研究生。根据中国科学院大学官方记载，已指导的学生包括：
| 姓名 | 学位类型 | 专业 |
|---|---|---|
| 陈靖 | 博士研究生 | 081202-计算机软件与理论 |
| 刘剑 | 博士研究生 | 081202-计算机软件与理论 |
| 吴鹏 | 博士研究生 | 081202-计算机软件与理论 |
| 陈义 | 博士研究生 | 081203-计算机应用技术 |
| 郑维 | 博士研究生 | 081202-计算机软件与理论 |
| 刘大光 | 硕士研究生 | 081202-计算机软件与理论 |
| 邓维佳 | 硕士研究生 | 081202-计算机软件与理论 |
此外，林惠民作为首席教授在中国科学院大学开设了《并发数据结构与多核编程》课程，该课程由吕毅、吴鹏、杨潇潇等教师共同主讲，从原理和实践两方面讲授面向多核系统的程序设计方法。该课程于2021年被评为中国科学院大学校级"研究生优秀课程"，年平均约8%的选课学生来自非计算机专业，在交叉学科培养方面具有显著特色。
林惠民培养的学生和团队成员在形式化方法、并发理论、模型检测等领域继续深耕，形成了以软件所为基地的形式化方法研究学派。此外，实验室同一时期培养的代表性学者詹乃军（周巢尘院士的博士生，1997-2000年在软件所获博士学位）后来成长为中科院软件所研究员、计算机科学国家重点实验室执行主任，现兼任北京大学计算机学院博雅特聘教授，并担任CCF形式化方法专委会主任，成为该领域的重要学术带头人。
四、学术合作网络
4.1 内部合作（软件所团队）
中国科学院软件研究所计算机科学国家重点实验室（现已整合为基础软件与系统重点实验室）是中国形式化方法研究的核心基地，汇聚了以林惠民院士为首的多位形式化方法领域的杰出学者，形成了实力雄厚的研究团队：
- 周巢尘：中国科学院院士，时段演算（Duration Calculus）的创始人之一，长期从事时序逻辑和实时系统形式化验证研究。周巢尘与林惠民同为软件所形式化方法研究的奠基人，两人共同构成了实验室在并发理论和形式化方法领域的学术双峰。
- 詹乃军：中科院软件所研究员（现兼任北京大学博雅特聘教授），国家杰出青年科学基金获得者。1997-2000年在软件所获博士学位（导师周巢尘院士），研究方向包括形式化方法、实时嵌入式混成系统、程序验证等。担任CCF形式化方法专委会主任、多个国际会议（FM 2021、TACAS 2027等）程序委员会共同主席，在著名国际会议和杂志发表论文150多篇。詹乃军从博士阶段即受周巢尘等老一辈科学家指导，同时亦受到林惠民等实验室前辈的学术熏陶，是软件所形式化方法学术传承的重要代表。
- 吴志林：研究员、博士生导师。2002-2007年在软件所计算机科学国家重点实验室硕博连读获博士学位，研究方向为计算机软硬件基础设施形式化验证、计算逻辑、自动机理论。2020年获"CCF-IEEE CS青年科学家奖"，参与研制的字符串约束求解器OSTRICH获2023年国际SMT求解器竞赛字符串理论第一名。担任CCF形式化方法专委会秘书长，在LICS、POPL、CAV等顶级会议发表论文40余篇。吴志林从博士阶段起即受实验室老一辈科学家（包括林惠民）的熏陶，是软件所自主培养的形式化方法中坚力量。
- 张立军：研究员、博士生导师，中国科学院大学特聘教授。2000-2008年在德国萨尔大学获博士学位，回国前曾任牛津大学助理研究员、丹麦科技大学副教授。2013年加入软件所，主要从事概率模型检验、形式化方法和智能算法可靠性研究，带领团队开发了概率模型验证工具ePMC。2022年获中科院稳定支持基础研究团队项目资助，负责研究开放环境下的可信智能算法。在CAV、CONCUR、LICS、POPL等顶级会议和期刊发表大量论文。
4.2 跨机构合作
林惠民及软件所形式化方法团队与国内多所高校和科研机构保持着密切的合作关系：
- 北京大学：詹乃军教授现兼任北京大学计算机学院博雅特聘教授，与软件所团队保持深度合作。此外，北京大学的胡振江教授、曹永知教授等也经常与软件所团队在形式化方法和软件验证领域展开合作交流。在CCF秀湖会议等学术活动中，林惠民院士多次与北京大学学者共议形式化方法的发展。
- 上海交通大学：陈海波教授（操作系统形式化验证方向）与软件所团队在基础软件验证领域有密切合作。陈海波曾作为执行主席之一参与组织CCF秀湖会议，与林惠民院士共同探讨大型基础软件形式化验证问题。
- 华东师范大学：张民教授等在形式化方法领域与软件所团队保持长期合作，张民担任CCF形式化方法专委会副主任委员（执行）兼办公室主任。
- 国防科技大学：董威教授、陈振邦教授等在程序验证和形式化方法领域与软件所开展合作。董威担任CCF形式化方法专委会副主任委员。
- 华为技术有限公司：在CCF秀湖会议中，华为诺亚方舟实验室主任李震国、华为费马实验室主任秦胜潮等与林惠民院士共同探讨形式化方法在工业界的应用。华为的付明等也是CCF形式化方法专委会的成员，体现了学术界与产业界在形式化验证领域的深度合作。
- 北京控制工程研究所：陈睿、董晓刚等在航天可信软件的形式化验证方面与软件所团队有密切合作，推动了形式化方法在航天领域的实际应用。
4.3 国际合作
林惠民的国际学术合作网络广泛，其学术生涯与英国计算机科学界有深厚渊源：
- 英国爱丁堡大学：1986-1987年，林惠民在爱丁堡大学计算机科学基础实验室从事博士后研究。爱丁堡大学是进程代数（CCS）创始人、图灵奖得主Robin Milner的工作单位。林惠民在此期间深入接触了进程代数理论研究的前沿，为他后来设计世界上第一个通用的进程代数验证工具奠定了重要基础。爱丁堡大学也是π-演算的发源地，林惠民后来解决了π-演算的有穷公理化问题，这一重要工作与这段经历密切相关。
- 英国萨塞克斯大学：1990-1993年，林惠民担任萨塞克斯大学Research Fellow，历时三年。这段经历使他与英国理论计算机科学界建立了深厚的学术联系。
- 翻译Milner著作：2009年，林惠民翻译了Robin Milner的著作《Communicating and Mobile Systems: the π-Calculus》（中译本《移动与通信系统：π-演算》，清华大学出版社），将π-演算理论系统地引介到中国学术界，进一步深化了中英在进程代数领域的学术交流。
- 符号互模拟理论：林惠民与国际同行合作提出、并独立发展了传值并发进程的"符号互模拟"理论，这一理论成果被国内外同行在公开发表的文献中广泛引用。他在Applied Pi Calculus方面的工作发表于Theoretical Computer Science等国际权威期刊。
- 国际学术交流：林惠民积极参与国际学术共同体建设，在CONCUR、CAV、TASE等重要国际会议的程序委员会中担任委员，与国际形式化方法社区保持着长期的合作关系。他培养的学生和团队成员也在LICS、POPL、CAV、FM等顶级国际会议发表论文，形成了具有国际影响力的学术网络。
五、业界合作关系深度分析
林惠民院士虽然从事的是理论计算机科学的基础研究，但其成果在工业界具有重要的应用价值，近年来积极推动形式化方法与产业需求的结合：
工业应用方向：林惠民在2024年CCF秀湖会议上作了题为"大型基础软件的形式化验证：问题与挑战"的特邀报告，强调了形式化验证在安全攸关大型基础软件中的不可替代性，并带领与会者探讨操作系统形式化验证实践中面临的挑战。这反映了他对将形式化方法应用于操作系统、编译器等基础软件验证的持续关注。
航天领域合作：林惠民团队与航天工业部门有密切合作。詹乃军教授主持的"东风微内核操作系统形式化验证"项目（航天科工四院重大型号项目，经费1750万元），完成了国产多核实时操作系统微内核的全流程验证工作，包括2.5万行系统源码验证、45万行Coq形式化验证代码开发、修正两百余项程序缺陷，助力该操作系统通过CC EAL5+安全认证。这是形式化方法在中国航天领域应用的标志性成果。
华为合作：在CCF形式化方法专委会的组织下，华为技术有限公司成为形式化方法产学研合作的重要伙伴。华为诺亚方舟实验室和费马实验室的研究人员积极参与专委会活动，推动形式化方法在通信、芯片设计等工业场景中的应用。软件所团队在RISC-V处理器验证、Chisel硬件描述语言验证等方面的研究成果也与芯片产业紧密相关。
国家重大项目：林惠民主持了国家级科研项目"模型检测的理论、技术与工具"（2009-2012），并推动了多项形式化方法相关国家重点研发计划项目的实施。其团队成员承担了国家重点研发计划项目"安全攸关软件框架验证的数学方法与应用"（1490万元）、国家自然科学基金重大项目等多项重要科研任务，将形式化方法的理论成果转化为工程实践。
学科建设推动：林惠民院士积极推动计算机科学名词审定工作，在理论计算机科学分委会会议上强调名词收选和审定工作对学科建设和社会传播的重要性。他还于2016年发起软件所学术年会并持续担任学术委员会主任，为软件所的基础研究与产业应用搭建了重要的交流平台。
六、重要奖项与学术兼职
主要奖项：
| 年份 | 奖项名称 | 级别 |
|---|---|---|
| 1996 | 中国科学院自然科学一等奖 | 院级 |
| 1999 | 国家自然科学二等奖（"并发进程的代数理论及验证工具"） | 国家级 |
| 1999 | 当选中国科学院院士 | 学术荣誉 |
| 2008 | 当选第一届中国计算机学会（CCF）会士 | 学术荣誉 |
| 2021 | 指导课程《并发数据结构与多核编程》获评国科大"研究生优秀课程" | 教学荣誉 |
学术兼职：
- 中国科学院软件研究所学术委员会主任
- 计算机科学国家重点实验室主任（曾任）
- 中国计算机学会（CCF）形式化方法专业组/专委会主任（曾任），现为CCF会士
- 中国计算机名词审定委员会理论计算机科学分委会顾问
- 多个国际学术会议程序委员会委员
- 曾主持CNCC2024大会特邀报告等多个重要学术会议
林惠民院士在1999年当选中科院院士时年仅52岁，是该领域最年轻的中科院院士之一。2008年与李未、梅宏等一同当选第一届中国计算机学会会士，彰显了他在中国计算机科学界的崇高学术地位。近年来，他频繁受邀在CNCC等大规模学术会议上作特邀报告（如2024年CNCC特邀报告"计算、智能、安全"），持续发挥着学科引领作用。
七、Connection圈层总结
林惠民院士的学术关系网络呈现出一个以软件所为核心、向外辐射至国内外学术界和工业界的多层次结构：
核心圈层（软件所形式化方法团队）：以林惠民院士为学术领袖，周巢尘院士为共同奠基人，詹乃军研究员（现兼任北京大学博雅特聘教授）、吴志林研究员、张立军研究员等为中坚力量的研究团队。这一团队覆盖了进程代数、时段演算、模型检测、程序验证、概率系统验证等形式化方法的主要研究方向，形成了中国最完整的形式化方法研究体系。
学术传承圈层（学生与合作者网络）：林惠民指导的博士生（陈靖、刘剑、吴鹏、陈义、郑维等）及间接培养的青年学者构成了中国形式化方法研究的第二代和第三代力量。詹乃军（师承周巢尘院士）作为软件所形式化方法学术传承的杰出代表，已成为国家杰青获得者、CCF形式化方法专委会主任，在北京大学继续推动这一领域的学术发展。吴志林作为实验室自主培养的学者，获得了CCF-IEEE CS青年科学家奖，代表了新一代形式化方法研究者的成长。
国内合作圈层（高校与科研院所）：通过CCF形式化方法专委会、CCF秀湖会议、软件所学术年会等平台，林惠民及团队与北京大学、上海交通大学、华东师范大学、国防科技大学、南京大学、西安电子科技大学、清华大学等多所高校建立了广泛的学术合作关系，形成了覆盖全国的形式化方法研究协作网络。
国际合作圈层（英欧学术网络）：以爱丁堡大学和萨塞克斯大学的学术经历为起点，林惠民与英国理论计算机科学界建立了深厚联系，特别是与Robin Milner创立的进程代数和π-演算研究传统一脉相承。团队成员在法国波尔多大学、巴黎第七大学、德国萨尔大学、丹麦科技大学、牛津大学等欧洲院校的博士后或访问经历，进一步拓展了国际学术合作网络。
产业应用圈层（航天与信息技术领域）：通过航天科工集团的操作系统形式化验证项目、华为公司的产学研合作、以及芯片设计验证等方向，林惠民团队的形式化方法研究成果正在向国家关键信息基础设施的安全保障领域转化，体现了基础理论研究对国家重大战略需求的支撑作用。
林惠民院士历经从工人到院士的传奇人生，以近四十年的学术坚守，在中国形式化方法领域开辟了一片学术沃土。他的学术影响不仅体现在个人的突破性研究成果上，更体现在他所构建的从理论到实践、从软件所到全国乃至国际的完整学术生态。随着人工智能和大型基础软件对形式化验证提出新的挑战和需求，林惠民所奠基的这一学术网络将继续在中国计算机科学的发展中发挥不可替代的重要作用。