南大软件所 卜磊 教授
报告生成时间： 2026年8月
个人主页： https://software.nju.edu.cn/bulei/index.html （南京大学软件学院页面；旧版主页 http://cs.nju.edu.cn/bulei/ ） DBLP： https://dblp.org/pid/64/5155.html Google Scholar： 未找到可确认归属的公开页面
一、学者基本信息
卜磊（Bu Lei），南京大学教授、博士生导师，南京大学软件学院副院长（2022年7月至今）。他出身于南京大学计算机学院软件工程组（SEG，李宣东教授领衔，软件新技术全国重点实验室核心团队），长期从事形式化方法与软件工程研究，是南大"并发理论—模型检测—信息物理融合系统验证"方向（李宣东—赵建华一系）的代表性中坚力量。兼任中国计算机学会（CCF）系统软件专业委员会秘书长。
教育与工作经历（依据其个人主页）： - 2000-2004年，南京大学计算机科学与技术系学士。 - 2004-2006年，南京大学硕士（导师：李宣东教授）。 - 2006-2010年，南京大学博士（导师：李宣东教授）。 - 2006年，美国德克萨斯大学达拉斯分校（UTD）访问学生（合作者：W. Eric Wong教授）。 - 2007-2008年，卡内基梅隆大学（CMU）访问学生（合作者：Edmund M. Clarke教授，模型检测学派创始人、图灵奖得主）。 - 2014-2015年，微软亚洲研究院"铸星计划"访问学者（软件分析组）。 - 2010年起任南京大学助理教授，2013年晋升副教授，2018年晋升教授；2022年7月起任软件学院副院长。
荣誉与人才计划（依据其个人主页）： - 国家级青年人才计划（2024年） - CCF-IEEE CS青年科学家奖（2022年） - 中创软件人才奖（2023年） - NASAC青年软件创新奖（2019年） - 教育部计算机类专业教学指导委员会"高校计算机专业优秀教师奖励计划"（2020年） - CCF青年人才发展计划（2016年）、微软亚洲研究院"铸星计划"（2014年）
研究主线与代表性贡献： 1. （线性）混合系统可达性分析： 围绕线性混合自动机的有界可达性判定提出系列高效算法（STTT 2011、TC 2017、FMSD 2014等），是国际上该方向的持续贡献者。 2. CPS形式化验证与预期功能安全： 面向智能汽车/信息物理融合系统的安全性验证（SOTIF评估，TCAD 2026；场景建模与反例制导证伪，CAV 2024），并参与组织ARCH国际CPS验证竞赛系列研讨会。 3. 并发模型与业务流程： 早期从事时序一致性检查（FORTE 2006）与BPM业务流程模型分析，近年扩展至实时系统验证。 4. 智能化软件工程： 近年将LLM引入形式规约自动生成（SpecGen，ICSE 2025；SpecEval）、代码意图修复（ICSE 2025）、多模态语音助手测试（TSE 2026）等，形成"形式方法+AI"的新主线。
二、DBLP数据统计
2.1 发表记录总览
DBLP pid为64/5155，共收录105条记录（截至2026年8月）：会议论文64篇、期刊论文37篇、会议论文集编辑3条、书籍章节1条；其中CoRR/arXiv预印本13篇。DBLP记录起于2005年（其硕士阶段），覆盖从时序一致性检查到混合系统验证再到LLM驱动软件工程的完整演进。无同名混淆问题（"Lei Bu"在DBLP中唯一指向本人）。
2.2 年度产出分布
| 年份 | 论文数 | 年份 | 论文数 | 年份 | 论文数 |
|---|---|---|---|---|---|
| 2005 | 1 | 2012 | 10 | 2019 | 6 |
| 2006 | 2 | 2013 | 2 | 2020 | 4 |
| 2008 | 1 | 2014 | 5 | 2021 | 5 |
| 2009 | 1 | 2015 | 1 | 2022 | 8 |
| 2010 | 5 | 2016 | 3 | 2023 | 7 |
| 2011 | 6 | 2017 | 4 | 2024 | 9 |
| — | — | 2018 | 8 | 2025 | 12（2026年再5条） |
趋势分析： 2005-2011年为博士阶段与入职初期，产出集中于形式化验证基础工作；2012年（10条）为博士后期峰值；2013-2017年进入稳定期；2018年起随CPS验证与国际化合作扩展再度上升，2025年12条创单年新高，反映其"形式方法+LLM"新方向和学生梯队（刘尚青、马乐之、李苏皖等）成熟带来的产出加速。2024-2026年合计26条，为生涯最密集阶段。
2.3 主要发表会议/期刊分布（非CoRR）
| 会议/期刊 | 论文数 | 级别 |
|---|---|---|
| ASE | 6 | CCF-A |
| ISSTA | 4 | CCF-A |
| ICSE | 3 | CCF-A |
| ICCPS | 4 | 未入CCF目录（CPS旗舰会议） |
| IEEE TCAD | 3 | CCF-A |
| DATE | 3 | CCF-B |
| Internetware | 3 | CCF-C |
| HSCC | 2 | CCF-B |
| VMCAI | 2 | CCF-B |
| ACM TCPS | 2 | 未入CCF目录（CPS重要期刊） |
| IEEE TC | 3 | CCF-A |
| IEEE TPDS | 2 | CCF-A |
| IEEE TSE | 1 | CCF-A |
| FMCAD | 2 | CCF-B |
| CAV | 1 | CCF-A |
| TACAS | 1 | CCF-B |
| FM | 1 | CCF-B |
| ICRA | 1 | CCF-B |
| 其他（ARCH系列、SETTA、APSEC、STTT、FACS等） | 约30 | - |
分布特征： 发表呈现"验证理论会议（CAV/TACAS/VMCAI/HSCC/FMCAD/DATE）+软工顶会（ASE/ISSTA/ICSE）+CPS专题（ICCPS/ARCH）"三线并进结构。ASE与ISSTA合计10条，显示其测试与验证交叉选题在软工顶会的稳定落点；2025年后ICSE/ASE/TSE论文集中于LLM驱动的规约生成与测试方向。
2.4 合作者网络总览
105条记录对应193位唯一合作者，网络规模在软件所教师中居前列。结构呈"SEG双核（李宣东、赵建华）—国际验证学界（Abate/Frehse/Zaffanella等）—青年梯队（刘尚青、马乐之、王嘉万等）—跨机构延伸（UQ白广东、NTU刘杨、中科大Kai Chen等）"四个层次。李宣东以46次合作贯穿其全部学术生涯；赵建华（17次）为SEG资深同事；国际合作伙伴以欧洲混合系统验证学派（牛津大学、维也纳工业大学、维罗纳大学）为主轴。
2.5 核心合作者（Top 25，按DBLP合作频次降序）
| 排名 | 合作者（DBLP名） | 合作次数 | 合作年份 | 身份/机构与关系 |
|---|---|---|---|---|
| 1 | Xuandong Li（李宣东） | 46 | 2005-2025 | SEG创始人之一、计算机学院原院长，硕士与博士双阶段导师 |
| 2 | Jianhua Zhao（赵建华） | 17 | 2005-2025 | SEG教授，博士答辩委员会成员、资深同事 |
| 3 | Shangqing Liu（刘尚青） | 14 | 2024-2026 | 博士生（已毕业，现任昆士兰大学讲师），规约生成/验证方向 |
| 4 | Xin Chen | 14 | 2010-2021 | 博士生（已毕业），混合系统验证 |
| 5 | Linzhang Wang（王林章） | 14 | 2008-2020 | SEG教授、同事，测试与验证方向 |
| 6 | Qixin Wang | 10 | 2011-2023 | 博士生（已毕业），实时系统验证 |
| 7 | Jiawan Wang | 7 | 2019-2026 | 博士生，CPS场景建模与证伪（CAV 2024） |
| 8 | Guangdong Bai（白广东） | 7 | 2021-2026 | 昆士兰大学讲师（南大校友），VUI/安全测试方向跨国合作 |
| 9 | Suwan Li | 6 | 2022-2026 | 博士生，语音应用测试 |
| 10 | Kai Chen（陈凯） | 6 | 2022-2026 | 中国科学技术大学教授，CPS安全测试合作 |
| 11 | Xiaofei Xie | 6 | 2024-2025 | 新加坡国立大学助理教授（原MSRA），LLM+程序分析合作 |
| 12 | Feng Tan | 6 | 2012-2019 | 博士生（已毕业），混成系统验证 |
| 13 | Yuming Wu | 5 | 2019-2025 | 博士生，混合自动机可达性 |
| 14 | Alessandro Abate | 5 | 2017-2023 | 牛津大学教授，混合系统验证国际合作核心 |
| 15 | Goran Frehse | 5 | 2017-2023 | 美国圣母大学/原Verimag，d/dt工具作者 |
| 16 | Shaopeng Xing | 5 | 2019-2022 | 博士生（已毕业） |
| 17 | Rajarshi Ray | 5 | 2017-2022 | 印度研究者，ARCH合作 |
| 18 | Fuman Xie | 4 | 2022-2026 | 合作研究者，语音测试 |
| 19 | Lezhi Ma | 4 | 2024-2026 | 博士生，SpecGen规约生成（ICSE 2025） |
| 20 | Limin Wang | 4 | 2023-2025 | 合作研究者 |
| 21 | Stefan Schupp | 4 | 2017-2023 | 维也纳工业大学，HyPro工具团队 |
| 22 | Enea Zaffanella | 4 | 2018-2022 | 维罗纳大学，PPL作者之一 |
| 23 | Dieky Adzkiya | 4 | 2017-2020 | 印尼泗水理工学院，区间计算合作 |
| 24 | Neeraj Suri | 4 | 2013-2019 | 达姆施塔特工业大学教授 |
| 25 | Xue Liu（刘学） | 4 | 2012-2019 | 麦吉尔大学教授，实时系统合作 |
三、博士教育背景与导师追溯
3.1 南京大学本硕博一贯制（2000-2010）
卜磊是SEG"郑国梁—李宣东"谱系的内生培养代表：2000-2004年本科、2004-2006年硕士、2006-2010年博士均在南京大学完成，硕博导师均为李宣东教授。博士期间两次重要国际访问塑造其学术网络：2006年赴UTD与W. Eric Wong（软件测试与缺陷定位专家）合作；2007-2008年赴CMU访问Edmund M. Clarke（模型检测创始人、2007年图灵奖得主）。其首篇DBLP记录（2005年，SDL Forum）即与李宣东、赵建华、郑国梁等署名。
3.2 学术谱系定位
徐家福（中国软件学先驱）
└─ 郑国梁（SEG创始人，南京大学教授）
└─ 李宣东（SEG负责人、计算机学院原院长）
└─ 卜磊（博士2010届，软件学院副院长、教授）
├─ Xin Chen、Qixin Wang、Feng Tan、Shaopeng Xing（已毕业博士）
└─ 刘尚青（UQ讲师）、Jiawan Wang、Lezhi Ma、Suwan Li、Yuming Wu（现役梯队）
└─ （平行线）赵建华（SEG教授，卜磊博士答辩委员会成员与长期同事）
CMU访问是其谱系中的关键"外部注入"：与Edmund Clarke的模型检测传统建立直接连接（Clarke于2020年去世，合作以2007-2008年访问期为主）。
3.3 与上游导师网络的关系
| 上游节点 | 与卜磊的关系 | DBLP直接合作 | 合作特征 |
|---|---|---|---|
| 李宣东 | 硕士与博士双导师 | 46次（2005-2025） | 形式化方法、并发理论、SEG团队全程合作 |
| 赵建华 | 资深同事、答辩委员会成员 | 17次（2005-2025） | 模型检测、不变式生成 |
| 郑国梁 | SEG创始人、早期署名合作者 | 2次（2005-2006） | 早期时序一致性研究 |
| Edmund M. Clarke | CMU访问合作导师 | 访问期间合作 | 模型检测学派连接 |
| W. Eric Wong | UTD访问合作者 | 访问期间合作 | 软件测试方向 |
四、团队合作网络
4.1 教师与导师同事层（SEG/软件所）
| 教师 | 合作次数 | 合作年份 | 角色 | 主要交集 |
|---|---|---|---|---|
| 李宣东 | 46 | 2005-2025 | 博士导师、SEG负责人 | 形式化方法、并发理论全方向 |
| 赵建华 | 17 | 2005-2025 | SEG资深教授 | 模型检测、混成系统 |
| 王林章 | 14 | 2008-2020 | SEG教授 | 测试、业务流程建模 |
| Xiao Guo | 3 | 2022-2024 | SEG相关青年研究者 | JVM测试、混成系统 |
| 王慧妍 | - | - | 软件所准聘助理教授 | 同所同事（直接论文合作有限） |
| 马晓星、许畅、曹春、李樾等 | 少量 | - | 软件所其他小组负责人 | 同属软件所（另有独立报告） |
团队组织特征： 卜磊的网络主体是SEG（软件工程组），而非曹春所在的I2Ec系统组或李樾的PASCAL组；三个组同属软件所（软件新技术全国重点实验室），共享吕建院士—郑国梁—徐家福的上游谱系。蒋炎岩（iSE实验室）与黄宇（DisAlg小组）同为软件所同事，均另有独立PI报告，与卜磊的直接论文合作较少。
4.2 学生与青年成员层
| 成员 | 合作次数 | 方向/代表性交集 |
|---|---|---|
| 刘尚青 | 14 | LLM形式规约生成（SpecGen，ICSE 2025）、SOTIF；现任昆士兰大学讲师 |
| Xin Chen | 14 | 混合系统有界可达性（早期主力） |
| Qixin Wang | 10 | 实时系统、混成系统验证 |
| 王嘉万 | 7 | CPS场景建模与可扩展证伪（CAV 2024） |
| 马乐之 | 4 | SpecGen/SpecEval、LLM规约合成 |
| 李苏皖 | 6 | 多模态语音助手VUI测试（TSE 2026） |
| 吴宇明 | 5 | 组合式线性混合自动机可达性（TECS 2025） |
| 谭峰 | 6 | 混成系统验证、ARCH竞赛 |
| Shaopeng Xing | 5 | 混合系统可达性 |
| Qi Guo、Xiaohong Li、Chang Yue等 | 3-4 | 代码修复、工业场景合作研究 |
（注：上表为学生/青年梯队推断，其中刘尚青的师生关系与现职有公开履历佐证，其余成员身份系由SEG长期署名模式推断，仅凭论文署名不能认定师生关系；部分英文名的中文写法为惯例音译，以DBLP英文署名为准。）
4.3 人才培养
卜磊培养了多届SEG博士，毕业去向呈"国际高校+本校接力"特征：刘尚青现任澳大利亚昆士兰大学讲师（并与UQ白广东形成持续的南大—UQ论文通道）；其他已毕业博士的去向公开资料未系统性披露。其主导或参与的教学成果获教育部教指委"高校计算机专业优秀教师奖励计划"（2020）。作为软件学院副院长，他还承担软件学院的教学组织工作。
五、业界合作关系深度分析
5.1 微软亚洲研究院——"铸星计划"通道
2014-2015年卜磊入选微软亚洲研究院"铸星计划"，在软件分析组进行访问研究。该经历使其与MSRA系研究者（如谢晓菲，原MSRA、现NUS助理教授）建立长期合作——2024-2025年二人在ICSE 2025（SpecGen）、ISSTA 2024（FT2Ra）等论文上持续联合署名，是当前其最活跃的国际合作通道之一。
5.2 智能汽车与CPS安全方向的应用牵引
其近年CPS验证工作面向智能汽车预期功能安全（SOTIF）：TCAD 2026论文（STPA引导的自动驾驶实时行为SOTIF评估）、CAV 2024论文（面向机器人系统的场景建模与证伪）均属该主线。该方向与国家智能网联汽车安全需求高度对应，属"问题牵引"型产学研接口；但论文合作者（如Yulong Lv等）的机构归属在公开页面未标注，具体合作企业主体公开资料未披露。ISSTA 2024论文FT2Ra等LLM软件工程工作的作者名单中亦包含疑似企业背景研究者（DBLP署名未标注机构），同样无法从公开资料确认具体企业。
5.3 国际学术界合作网络（区别于产业合作）
- 欧洲混合系统验证学派： 牛津大学Alessandro Abate（5次）、维也纳工业大学Stefan Schupp（4次，HyPro工具）、维罗纳大学Enea Zaffanella（4次）、原Verimag的Goran Frehse（5次，d/dt工具）——围绕ARCH（Applied Verification for Continuous and Hybrid Systems）国际研讨会的持续协作圈。
- 亚洲合作者： 中科大陈凯（6次，CPS安全）、NTU刘杨（Yang Liu，3次，自演化软件路线图）、NUS谢晓菲（6次）、UQ白广东（7次）。
- 美国合作者： 达姆施塔特Neeraj Suri（4次）、麦吉尔刘学（4次）——早期实时系统合作。
5.4 产业问题与技术路线对应
| 应用约束 | 技术议题 | 证据强度 |
|---|---|---|
| 智能汽车预期功能安全验证 | STPA引导SOTIF评估、场景证伪 | 论文主题明确，合作企业未披露 |
| 大模型辅助软件工程落地 | 规约自动生成、代码意图修复 | ICSE/ASE/TSE论文，企业合作者署名存在但归属未披露 |
| CPS/机器人安全性 | 有界可达性、反例制导验证 | 学术合作主导（ARCH圈子） |
六、Connection圈层总结
第一圈层——SEG师承核心： 李宣东（46次）是贯穿其2005年以来全部学术生涯的中心节点；赵建华（17次）作为答辩委员会成员与资深同事构成第二支点。卜磊是"南大本硕博一贯制+国际顶级访问（Clarke/Wong/MSRA）"组合培养的典型SEG二代教师。
第二圈层——国际验证学界： 以ARCH研讨会为纽带的欧洲混合系统验证学派（Abate、Frehse、Schupp、Zaffanella）与其保持了2017-2023年的密集合作；CMU模型检测传统经其访问经历注入SEG。
第三圈层——学生梯队与跨机构通道： 刘尚青（14次，UQ讲师）、王嘉万、马乐之、李苏皖、吴宇明等构成现役产出主力；"南大—UQ（白广东—刘尚青）"、"南大—NUS（谢晓菲）"、"南大—NTU（刘杨）"、"南大—中科大（陈凯）"四条跨机构通道支撑其2024-2026年的高产出。
第四圈层——软件所同事生态： 与曹春（I2Ec）、李樾/谭添（PASCAL）等同所教师分属不同小组，通过软件所（软件新技术全国重点实验室）的组织框架形成弱连带；蒋炎岩、黄宇等同事另有独立PI报告。
第五圈层——业界接口： MSRA铸星计划（2014-2015）是其明确的产业合作经历；智能汽车SOTIF与LLM软件工程方向存在工业合作迹象，但具体企业主体公开资料未披露。
产出规模与发展阶段： 105条DBLP记录、193位合作者，为软件所教师中网络最广者之一。2025-2026年的产出峰值（17条）显示其正处"形式方法+LLM"新方向的加速期；作为软件学院副院长与CCF系统软件专委秘书长，其行政与学术服务角色亦处于上升期。
七、数据来源与局限性说明
本报告主数据来自DBLP作者记录（pid: 64/5155），并结合以下公开信息源：
- 卜磊个人主页（https://software.nju.edu.cn/bulei/index.html ：教育经历、访问经历、荣誉、任职时间线）
- SEG软件工程组主页（https://seg.nju.edu.cn/ ：组史、成员规模、李宣东团队信息）
- 南京大学计算机软件研究所组织页（https://ics.nju.edu.cn/centers/index.html ）
- DBLP作者搜索API及作者XML记录（发表统计、合作者统计）
- 论文页面（ICSE 2025 SpecGen、CAV 2024、TCAD 2026等署名信息）
- 南京大学计算机学院师资列表（博导身份）
局限性说明：
- DBLP记录含编辑条目： 105条记录中含3条会议论文集编辑记录（Internetware 2025、SETTA 2024等程序委员会主席职务），非个人论文，统计时未单独剔除但已在正文说明。
- 学生身份判断： "学生与青年成员层"中刘尚青的师生关系与现职有公开履历佐证；其余成员身份系由署名模式推断，不能仅凭论文署名认定师生关系；部分合作者仅以拼音署名，中文名写法可能不准确，以DBLP英文署名为准。
- 业界合作归属未披露： 智能汽车SOTIF、LLM软件工程方向论文中的疑似企业合作者机构归属在DBLP与公开论文页面均未标注，报告不作企业归属推断。
- 职称与职务时效： 软件学院副院长职务依据其个人主页（2022年7月起）；"国家级青年人才计划"具体批次（2024年）依主页表述，未独立核实。
- 历史页面差异： 其旧版主页（cs.nju.edu.cn/bulei）与新主页（software.nju.edu.cn/bulei）均存在，部分经历描述以新主页为准。