中科院软件所形式化方法团队 学术关系网络报告

团队简介

本报告集涵盖中国科学院软件研究所形式化方法研究团队的学术关系网络。软件所拥有计算机科学国家重点实验室，是中国形式化方法研究的发源地和核心阵地。团队以周巢尘院士和林惠民院士两位学术泰斗为奠基人，历经数代传承，在时段演算、进程代数、实时/混成系统验证、SAT/SMT求解、软硬件形式化验证等方向产出了具有国际影响力的成果，并在航天、芯片设计、操作系统等安全攸关领域实现了产业落地。

报告清单

序号	姓名	职称	研究方向	报告文件
1	周巢尘	院士	时段演算、分布式程序理论、实时系统形式化	cas_iscas_zhouchaochen_network.md
2	林惠民	院士	并发理论、进程代数验证工具、π-演算	cas_iscas_linhuimin_network.md
3	詹乃军	研究员	实时/混成系统、CPS、程序验证	cas_iscas_zhannaijun_network.md
4	吴志林	研究员	软硬件形式化验证、约束求解、程序验证	cas_iscas_wuzhilin_network.md
5	蔡少伟	研究员	SAT/SMT求解、约束求解	cas_iscas_caishaowei_network.md

团队架构

团队学术传承主线为：胡世华院士（数理逻辑）→ 周巢尘院士（时段演算/分布式程序理论）→ 詹乃军研究员（混成系统/HCSP/CCEAL5+验证）。林惠民院士作为并列的学术双峰，在并发理论方向独立发展。詹乃军现任CCF形式化方法专委会主任，吴志林任秘书长，蔡少伟在SAT/SMT求解器方面取得国际竞赛冠军级成果。

蔡少伟的求解器已被NVIDIA、微软、英特尔、华为等公司集成使用，吴志林的RISC-V/Chisel验证技术已获多项专利，詹乃军主持的操作系统微内核形式验证助力通过CC EAL5+安全认证——三者构成了从底层求解器到系统级验证的完整产业应用链。

报告生成时间

2026年8月20日