软件所形式化 詹乃军 研究员
报告生成时间：2026年8月20日
个人主页：詹乃军
所属团队：中国科学院软件研究所 / 计算机科学国家重点实验室 / 北京大学博雅特聘教授
一、学者基本信息
| 项目 | 内容 |
|---|---|
| 姓名 | 詹乃军（Naijun Zhan） |
| 出生年月 | 1971年5月 |
| 现任职务 | 北京大学计算机学院博雅特聘教授（2024年起）；中科院软件所研究员、博士生导师 |
| 原任职务 | 中科院软件所计算机科学国家重点实验室常务副主任（执行主任）、中科院特聘研究员、国科大岗位教授 |
| 学术兼职 | CCF形式化方法专业委员会主任（2024—2027） |
| 人才称号 | 国家杰出青年科学基金获得者、国家自然科学基金优秀青年基金获得者、中科院特聘研究员 |
| 研究方向 | 实时与混成系统、信息物理融合系统（CPS）、形式化方法、程序验证、计算语义模型 |
| 代表成果 | 国际会议与期刊论文150余篇；专著2部（《混成系统的形式建模、分析与验证》《Formal Verification of Simulink/Stateflow Diagrams》）、编著4部、国内外专刊9辑 |
| 代表工具 | MARS工具链、HHL Prover（混成霍尔逻辑定理证明器）、HCSP形式建模框架 |
| H指数量级 | 形式化方法领域国际知名学者，长期担任CAV、TACAS、FM、RTSS、HSCC等百余家国际会议程序委员 |
二、教育背景与职业履历
教育背景：
- 1989—1993：南京大学数学系，学士（数理逻辑方向），打下严格的逻辑学训练基础；
- 1993—1996：南京大学计算机科学系，硕士；
- 1997—2000：中国科学院软件研究所，博士，师从周巢尘院士（时段逻辑Duration Calculus创始人），博士论文与联合国大学国际软件技术研究所（UNU-IIST）联合完成。
职业履历：
- 2001—2004：德国曼海姆大学数学与计算机科学学院助理研究员，从事并发理论与时序逻辑研究；
- 2004—2008：中科院软件所副研究员；
- 2008至今：中科院软件所研究员；
- 2016年起：中科院特聘研究员，后任计算机科学国家重点实验室常务副主任（执行主任）；
- 2024年起：北京大学博雅特聘教授（兼任），同时在软件所保持研究团队。
其履历呈现"数学—逻辑—计算机"的典型理论路线：从南京大学数理逻辑出发，经周巢尘的时段逻辑学派训练与德国曼海姆的欧洲并发理论熏陶，最终成长为国内混成系统形式验证的领军人物。学术访问足迹包括丹麦技术大学（DTU）、美国新墨西哥大学、新加坡南洋理工大学、UNU-IIST（多次）以及保加利亚科学院等，形成了横跨欧亚的国际网络。
三、学生培养情况
詹乃军长期在国科大和北大招收博士生，其培养的学生已形成国内混成系统验证的一支核心梯队：
- 薛白：博士毕业后经新加坡南洋理工大学、德国奥登堡大学（与Martin Fränzle合作）两站博士后，现为中科院软件所研究员、中科院特聘研究员、基础软件与系统重点实验室副主任，获中科院青年人才择优支持、软件所杰青（结题优秀），研究方向覆盖随机系统可达性分析与安全强化学习，是詹乃军在随机混成系统方向最直接的学术传承者；
- 王淑玲（Shuling Wang）：软件所研究员，与詹乃军合著Springer专著《Formal Verification of Simulink/Stateflow Diagrams》（2016），是MARS工具链与AADL+S/S协同建模方向的核心骨干；
- 詹博华（Bohua Zhan）：软件所研究员，主持交互式定理证明方向（Isabelle/Auto2、holpy），与詹乃军合作完成基于高阶UTP的CPS语义基础系列工作（ACM TOSEM 2023），并参与微内核形式验证项目；
- 安杰：软件所副研究员、博士生导师，主持国家高层次海外青年人才项目，入选中科院"率先行动"引才计划，此前在德国马普所与日本NII工作；
- 徐雄、赵恒军、张苗苗、杨腾顺、靳祥玉、陈明帅等：一批活跃的青年合作者，分布于软件所、北京理工大学、高校教职及UNU-IIST等机构，构成了HCSP建模、5G AKMA协议形式分析、实时自动机学习等方向的持续产出力量。
从学生去向看，其培养呈现出"扎根本土实验室—辐射高校院所"的特征，多名学生已入选国家级青年人才计划，学术谱系正在快速扩张。
四、学术合作网络
4.1 实验室内部合作
计算机科学国家重点实验室是国内形式化方法的重镇，詹乃军在其中处于枢纽位置：
- 周巢尘：中科院院士，詹乃军的博士导师，时段逻辑与DC形式体系的奠基人。师徒二人在《形式语义学导论》（Introduction to Formal Semantics，Academic Press，2017）上合著，学术传承关系是国内混成系统验证学派的主脉络；
- 林惠民：中科院院士，并发理论专家，曾任CCF形式化方法专委会首任主任（2015—2020），与詹乃军同属实验室理论核心，詹乃军接任专委会秘书长、主任，延续了该实验室在专委会的领导地位；
- 吴志林：研究员，现为基础软件与系统重点实验室常务副主任、CCF形式化方法专委会秘书长，与詹乃军在专委会事务和字符串约束求解等方向长期合作；
- 张立军：研究员，概率模型检测与量子计算专家，在2024 CCF形式化方法专委会战略研讨会等场合共同组织学术活动；
- 另与蔡少伟（SAT求解）、夏变兰等在约束求解与程序验证方向有密切合作。
4.2 跨机构合作
- 北京大学：2024年起以博雅特聘教授身份深度融入北大计算机学院与逻辑研究中心，与孙猛等在程序理论与形式化方法方向开展合作；
- 北京控制工程研究所、中国空间技术研究院：与顾斌总师团队、杨孟飞院士团队合作开展航天器控制系统形式化设计（详见第五章）；
- 华东师范大学：与蒲戈光（嵌入式系统形式验证）等在北京市科学技术奖联合提名及学术会议中形成协作；
- 国防科技大学：与王戟教授（前任CCF形式化方法专委会主任）在专委会事务上前后接力，共同组织2024年专委会战略研讨会；
- 华为费马实验室：与秦胜潮主任联合主办CCF形式化方法专委会战略研讨会，探索"AI for FM / FM for AI"的产学研方向；
- 南京大学、武汉大学、烟台大学、河南大学等高校：频繁受邀讲学（珞珈软件论坛、两校名师讲堂、CCF@U系列活动等），扩散学术影响。
4.3 国际合作
- 德国：曼海姆大学博士后经历奠定了其欧洲合作网络；与奥尔登堡大学Martin Fränzle合作持续二十年（混成系统可达性、随机微分方程可达避分析等，成果发表于IEEE TAC），并与亚琛工业大学Joost-Pieter Katoen（概率程序，OOPSLA 2023）等开展合作；
- UNU-IIST（澳门）：博士论文联合完成，多次访问，与周巢尘、Jean-Pierre Talpin（INRIA）等基于UTP的高阶统一理论保持长期合作（TOSEM、TCS、LMSCP系列论文）；
- 新加坡南洋理工大学：薛白现任NTU访问教授，C.-H. Luke Ong等构成稳定合作通道；
- 丹麦技术大学（DTU）、新墨西哥大学、保加利亚科学院：早年访问建立的实时系统与时序逻辑合作网络；
- 国际学术组织任职：FM 2021（形式化方法旗舰会议）程序委员会联合主席、TACAS 2027（验证顶会）程序委员会联合主席、SETTA 2016 PC联合主席、MEMOCODE 2018/2019与ICESS 2019一般联合主席，SETTA与MEMOCODE指导委员会成员，以及《Journal of Automated Reasoning》《Formal Aspects of Computing》《JLAMP》《Research Directions: Cyber-Physical Systems》《软件学报》《计算机研究与发展》《电子学报》《前瞻科技》等国内外期刊编委。
五、业界合作关系深度分析
詹乃军是国内少有的将形式化方法做到工业级落地规模的学者，其业界合作集中于航天、军工、核电等国家战略安全攸关领域。
（1）国产多核实时操作系统微内核形式验证——旗舰工程。 团队对某国产多核实时操作系统微内核开展全流程形式验证：覆盖任务管理与调度、中断与异常处理、任务同步与通信、核间通信与动态重构、时钟管理、权能访问控制、分区配置与分区通信等核心模块，总计2.5万行系统源码；开发了45万行Coq形式化验证代码（规模与seL4验证工程同一量级，seL4约为1万行C代码对应48万行证明）；排查并修正200余项程序缺陷，最终助力该操作系统通过CC EAL5+安全认证。这是国内操作系统微内核通过的最高等级安全认证之一，直接服务于航天与军工装备的自主可控需求。团队还提出了可大幅降低基础软件验证人力成本、提升自动化水平的新验证框架，面向后续规模化推广。
（2）航天器控制系统形式化设计——与北京控制工程研究所顾斌总师合作。 与北京控制工程研究所（航天五院502所）顾斌总师团队建立了长期深度合作：提出以AADL+Simulink/Stateflow（AADL+S/S）组合建模、自动转换为HCSP形式模型、经混成霍尔逻辑（HHL）及其定理证明器验证、再经精化规则生成SystemC/ANSI-C代码的"模型驱动安全攸关嵌入式系统形式设计"路线，并基于HUTP（高阶UTP）给出翻译的形式语义与正确性证明。该路线在MARS工具链中实现并应用于航天真实案例；近期双方还在《软件学报》联合发表"嵌入式软件IP通用模型"工作（作者含徐雄、王淑玲、詹博华、詹乃军、李晓锋、顾斌、董晓刚、杨孟飞等），并曾联合申报2023年度北京市科学技术奖（顾斌、董晓刚、李晓锋、詹乃军、蒲戈光等联合提名）。合作网络进一步延伸至中国空间技术研究院（杨孟飞院士团队）。
（3）航天、核电、军工安全攸关嵌入式系统形式设计。 上述方法体系面向航天器控制、核电仪控、军工装备等安全完整性等级要求极高的嵌入式场景推广，形成了"理论—工具—工程"的完整闭环，属于国内形式化方法在关键基础设施领域的代表性落地。
（4）模型驱动开发环境的工业部署。 MARS工具链（含HHL Prover、AADL+S/S转换、精化代码生成等）已在多个工业合作场景中部署试用；团队还完成5G AKMA认证与密钥管理协议的形式化分析（发表于SETTA 2021/JSA 2022），显示出向通信安全领域扩展的能力。
（5）与华为的产学研协作。 作为CCF形式化方法专委会主任，与华为费马实验室、华为可信领域科学家委员会联合举办2024年专委会战略研讨会（共同主席：王戟、詹乃军、秦胜潮），推动"AI for FM"与"FM for AI"方向的产业对接；软件所联合信工所举办的可信人工智能研讨会亦通过中科院PIFI计划引入国际团队，詹乃军担任中方组织者。
总体而言，其业界合作模式可概括为："总师/院所需求牵引 + 理论与工具自主供给 + 安全认证为交付标志"，合作伙伴高度集中于航天（五院502所、空间技术研究院）与国防工业体系，兼具学术深度与工程规模，是国内"形式化方法实战派"的标杆。
六、重要奖项与学术兼职
- 国家杰出青年科学基金获得者；国家自然科学基金优秀青年基金获得者；
- 中科院特聘研究员（2016年起）、中国科学院大学岗位教授；
- 北京大学博雅特聘教授（2024年起）；
- CCF形式化方法专业委员会：秘书长（2015—2020）→ 副主任（2020—2023）→ 主任（2024—2027），十年间完成从执行者到掌舵者的完整接棒；
- 联合申报/参与北京市科学技术奖等省部级奖励；
- 国际会议组织任职：FM 2021与TACAS 2027程序委员会联合主席、SETTA 2016 PC联合主席、MEMOCODE 2018/2019与ICESS 2019一般联合主席、SETTA与MEMOCODE指导委员会委员；
- 期刊编委：JAR、FAC、JLAMP、Research Directions: CPS、软件学报、计算机研究与发展、电子学报、前瞻科技等；
- 专著：《混成系统的形式建模、分析与验证》（Springer, 2013）、《Formal Verification of Simulink/Stateflow Diagrams》（Springer, 2016，与王淑玲、赵恒军合著）、《形式语义学导论》（Introduction to Formal Semantics，Academic Press，2017，与周巢尘合著）。
七、Connection圈层总结
- 第一圈层（学术血统与核心团队）：博士导师周巢尘院士（时段逻辑学派源头）+ 实验室同侪林惠民院士；在世系意义上，詹乃军是"周巢尘—UNU-IIST"一脉在中国本土最重要的传承节点。
- 第二圈层（学生与门生）：薛白、王淑玲、詹博华、安杰等已成长为研究员级骨干，赵恒军、张苗苗、徐雄、杨腾顺、陈明帅等青年学者分布于全国高校院所，形成"软件所混成系统验证学派"的第二、三代梯队。
- 第三圈层（院所同事与国内学术圈）：吴志林、张立军、蔡少伟等实验室同事；王戟（国防科大）、蒲戈光（华东师大）、孙猛（北大）、苏开乐（烟台大学）等构成CCF形式化方法专委会为核心的国内学术共同体。
- 第四圈层（工业界与国际网络）：北京控制工程研究所顾斌总师团队、中国空间技术研究院杨孟飞院士团队、华为费马实验室等产业与工程方；国际上则连接Martin Fränzle（德国奥尔登堡）、Joost-Pieter Katoen（亚琛）、Jean-Pierre Talpin（INRIA）、C.-H. Luke Ong（牛津/NTU）以及UNU-IIST、DTU等机构。
综合来看，詹乃军的connection网络呈现"三位一体"结构：以周巢尘学术血统为纵轴（学术传承），以CCF形式化方法专委会为横轴（国内共同体领导权），以航天军工重大工程为纵深（工业落地）。其从理论（混成霍尔逻辑、UTP语义）到工具（MARS、HHL Prover）再到工程（CC EAL5+微内核验证）的完整链条，使其成为中国形式化方法界兼具学派领袖与工程总师双重身份的关键节点人物。