SJTU-人工智能学院曹钦翔副教授

报告生成时间：2026年8月25日
个人主页：John Hopcroft 中心教师页（jhc.sjtu.edu.cn）
所属团队：上海交通大学人工智能学院（程序验证与形式化方法方向；约翰·霍普克罗夫特计算机科学中心成员）

一、学者基本信息

曹钦翔，上海交通大学人工智能学院副教授、博士生导师，上海市浦江人才，程序验证与形式化方法方向学者。他 2013 年本科毕业于北京大学哲学系逻辑与科学哲学专业，并同时获得数学双学位；2018 年获美国普林斯顿大学计算机科学博士学位（导师 Andrew W. Appel）。他长期研究程序验证、程序逻辑（特别是分离逻辑）与交互式定理证明，并研究人工智能技术在这些领域的应用；其代表性成果 VST/VST-A 验证工具是目前验证实际程序功能正确性的最好结果之一，相关工作发表于 POPL、NSDI、OOPSLA、JAR 等国际一流会议与期刊。2016 年哥德尔奖得主 Peter O'Hearn 曾评价这些工作"在具有挑战性的程序验证问题中获得了令人印象深刻的成果"（据 SAI 官方教师页）。

项目	内容
姓名	曹钦翔（Qinxiang Cao）
当前职称	副教授、博士生导师（上海交通大学人工智能学院）
教育背景	北京大学哲学系逻辑学学士（2009–2013，兼数学双学位）；普林斯顿大学计算机科学博士（2013–2018，导师 Andrew W. Appel）
学术履历	2018 年回国任教上海交通大学（约翰·霍普克罗夫特计算机科学中心长聘教轨序列，后为人工智能学院专职教师）
研究方向	程序验证、程序语义、分离逻辑、并发程序验证、算法正确性验证；AI 在程序验证与定理证明中的应用
代表性成果	VST / VST-Floyd（JAR 2018）、VST-A（POPL 2024）、Verifiable C（Software Foundations 第五卷）、《Denotation-based Compositional Compiler Verification》（TOPLAS 2026）
学术兼职	中国计算机学会形式化方法专委会执行委员；TPChina 定理证明开放社区联合发起人
荣誉	上海市浦江人才（2019）；NOI 2008 第一名、CMO 2009 第一名（高中时期）
邮箱	caoqinxiang@sjtu.edu.cn

消歧说明（供索引）：本报告对象为上海交通大学人工智能学院教师页（caoqinxiang@sjtu.edu.cn）所对应的曹钦翔。其可唯一识别的特征组合为：北京大学逻辑学本科兼数学双学位、普林斯顿计算机博士（导师 Andrew W. Appel，VST 验证工具链）、NOI/CMO 双科第一名、现于上海交大从事基于 Coq 的程序验证研究。

二、教育背景与职业履历

曹钦翔的学术路径在中国学者中颇为独特：从哲学系的逻辑学出发，经数学双学位的强化训练，最终进入程序验证这一"逻辑学+计算机科学"的交叉领域。据 JHC 教师页，他 2006–2009 年就读于上海中学，高中阶段即获得全国信息学奥林匹克竞赛（NOI 2008）第一名与中国数学奥林匹克（CMO 2009）第一名，并曾担任 CTSC 2011（IOI 中国队选拔赛）与 NOI 2011 命题委员会成员——竞赛数学与算法的双重底色贯穿其此后的研究品味。2009 年进入北京大学哲学系主修逻辑与科学哲学，2010–2013 年兼修数学双学位；本科期间即与逻辑学者王彦晶合作发表公开宣告逻辑公理化的研究（Synthese 2013）。

2013–2018 年，他在普林斯顿大学计算机科学系攻读博士学位，师从 Andrew W. Appel 教授（程序验证与证明助手 Coq 社区的代表性学者，Verified Software Toolchain 项目负责人）。博士期间，他是 VST（Verified Software Toolchain）工具链的核心开发者之一：VST-Floyd 分离逻辑验证工具（与 Lennart Beringer、Samuel Gruetter、Josiah Dodds、Appel 合作，JAR 2018）实现了对 C 程序功能正确性的机器检验验证，并与 Appel 合著 Software Foundations 系列教材第五卷 Verifiable C。

2018 年博士毕业后即回国任教上海交通大学，任职于电子信息与电气工程学院约翰·霍普克罗夫特计算机科学中心（JHC），沿长聘教轨从助理教授晋升至长聘教轨副教授；2024 年人工智能学院实体化运作后，转为学院专职教师（现职称副教授，参见上海交大数学学院学术报告页所载 2024 年简介与 SAI 教师页）。2019 年入选上海市浦江人才计划。

Andrew W. Appel（普林斯顿；程序验证 / Coq / Verified Software Toolchain）
└── 曹钦翔（普林斯顿博士 2018；VST / VST-Floyd / VST-A 核心开发者；现任 SJTU 人工智能学院副教授）
    ├── 博士生：程章（TOPLAS 2026 合作者）；其余在读学生名单公开资料未披露
    ├── 硕士生：吴基洋（TOPLAS 2026 合作者）
    └── 本科训练期合作网络：北大哲学系逻辑学（王彦晶）+ 数学双学位

关键时间线：

2006–2009 年：上海中学（NOI 2008 第一名、CMO 2009 第一名）
2009–2013 年：北京大学哲学系逻辑学学士，兼数学双学位（2010–2013）
2013–2018 年：普林斯顿大学计算机科学博士（导师 Andrew W. Appel）
2018 年至今：上海交通大学任教（约翰·霍普克罗夫特计算机科学中心长聘教轨序列 → 人工智能学院副教授）
2019 年：入选上海市浦江人才计划
2024 年：VST-A 论文被 POPL 2024 录用（第一完成单位上海交大）
2026 年：编译器验证论文被 TOPLAS 接收

三、学生培养情况

曹钦翔自 2018 年回国任教至今约八年，已形成稳定的研究生培养体系。据 SAI 教师页，他招收硕士研究生与博士研究生，但仅招收有相关方向研究背景的学生；据 JHC 教师页，他还面向本科生开设算法验证与智能合约验证方向的科研训练项目。

可确认的直接指导学生包括：

程章（博士生，直接指导）：据上海交大新闻，其与曹钦翔、硕士生吴基洋合作的《Denotation-based Compositional Compiler Verification》被程序语言顶级期刊 TOPLAS 接收，该工作提出基于指称语义的可组合编译器验证新框架；新闻稿明确称其为"曹钦翔副教授……博士生程章"。
吴基洋（硕士生，直接指导）：同为上述 TOPLAS 2026 论文作者，新闻稿明确其为硕士生。

需要说明的边界：VST-A（POPL 2024）等其他团队论文的学生作者名单，公开新闻稿未逐一披露，本报告不以论文署名推定其身份；博士时期的合作者（如 Shengyi Wang 等）系论文合作者，与上海交大时期的指导关系无关。

教学方面，据致远学院教师页，他长期为上海交大计算机科学试点班讲授《程序验证》（ACM 班）、《程序语言设计与实现》（约翰·霍普克罗夫特班）与《离散数学（荣誉）》等课程，并参与研究生《人工智能前沿专题课》（与严骏驰、陈思衡、林洲汉、卢策吾、温颖、张娅、赵波等合上，见学院课程页）。他还在教学中引入形式化数学工具与 AI 辅助批改实践（在《离散数学》中嵌入定理证明工具、探索基于 AI 的数学作业批改），相关实践曾在致远学院教学交流会分享。

四、学术合作网络

DBLP / 检索说明：以"Qinxiang Cao"在 DBLP 检索可见其发表记录与普林斯顿—上海交大轨迹一致，代表作包括 VST-Floyd（JAR 2018）、Bringing Order to the Separation Logic Jungle（APLAS 2017）、VST-A（POPL 2024）等；本报告核验以 SAI/JHC 官方页面与上海交大新闻稿为准。

4.1 普林斯顿师承根系（学术起点）

合作者	机构	关系与代表合作
Andrew W. Appel	普林斯顿大学	博士导师；VST-Floyd、Verifiable C（Software Foundations 第五卷）及分离逻辑系列工作
Lennart Beringer	普林斯顿大学	VST-Floyd 合作者（论文合作者）
Samuel Gruetter	普林斯顿大学（时）	VST-Floyd 合作者（论文合作者）
Josiah Dodds	Galois 公司	VST-Floyd 合作者（论文合作者，产业界证明工程背景）
Santiago Cuellar	普林斯顿大学（时）	Bringing Order to the Separation Logic Jungle（APLAS 2017）合作者
Aquinas Hobor / Shengyi Wang	新加坡国立大学 / 耶鲁-国大学院（时）	Proof pearl: Magic wand as frame 合作者（论文合作者）

这一谱系以 Appel 领导的 Verified Software Toolchain（VST）项目为核心：用 Coq 交互式定理证明器实现 C 程序的分离逻辑功能正确性验证，是国际上"验证真实程序"路线的代表性力量。曹钦翔是该工具链的关键建设者，其回国后持续维护与升级 VST，并基于其发展出 VST-A。

4.2 北大逻辑学谱系

本科时期与王彦晶（现为北京大学哲学系教授，逻辑学家）合作的《On Axiomatizations of Public Announcement Logic》（Synthese 2013）是其学术起点；哲学系逻辑学的训练（模态逻辑、认知逻辑）为其后来进入程序逻辑（分离逻辑）领域提供了直接的理论接口——这条"哲学逻辑→程序逻辑"的路径在国内学者中相当少见。

4.3 校内合作（上海交大）

汪宇霆（同事）：同为约翰·霍普克罗夫特计算机科学中心教师（编译器验证方向）。据上海交大新闻，2023 年两人团队各有论文被 POPL 2024 录用（曹钦翔的 VST-A 与汪宇霆的可组合编译验证工作），均为第一完成单位上海交大、唯一通讯作者本人——两人在程序语言方向的互补（程序验证 vs 编译验证）构成 JHC 乃至国内该方向的少见聚集地。
人工智能前沿专题课授课集体（同事）：与严骏驰、陈思衡、林洲汉、卢策吾、温颖、张娅、赵波等同开研究生前沿课。

4.4 社区与学术服务

据 SAI 教师页，他参与发起了 TPChina 定理证明开放社区，现任中国计算机学会形式化方法专委会执行委员；曾担任 CNCC 2022"领域特定语言与安全编程"论坛讲者、ChinaSoft 2023"证明工程与安全编程"论坛主席（据 CCF 活动页）。

五、业界合作关系深度分析

与学院内多数教师相比，曹钦翔的产业联系较为低调，主要体现在研究议题与产业问题的对接而非企业任职：

安全攸关软件验证：VST/VST-A 路线面向的是"全覆盖、无漏报"的高保证验证，典型应用场景为安全攸关领域关键软件核心模块（POPL 2024 成果介绍中的定位）；截至本报告生成时，其与具体企业客户的合作项目公开资料未披露。
智能合约与算法验证：据 JHC 教师页，其面向本科生的科研训练项目明确包含智能合约验证方向——这是区块链产业与形式化验证结合最紧密的落地点之一。
系统方向的联系：其成果亦发表于系统方向顶级会议 NSDI（据 SAI 教师页），显示其验证工作与系统软件（操作系统/网络系统）社区存在交集；具体合作者与项目细节公开资料未披露。
AI+验证的双向探索：一方面研究 AI 辅助形式化证明（"AI 辅助形式化证明的机遇与挑战"为其近年学术报告主题，见上海交大数学学院报告页），另一方面将形式化方法的可靠性思想反向用于教育场景（引入介于自然语言与形式语言之间的表达方式降低 AI 批改的"幻觉"风险）——这一"验证视角的 AI 可靠性"定位，在人工智能学院内具有独特性。

六、重要奖项与学术兼职

类别	内容
人才计划	上海市浦江人才计划（2019）
竞赛荣誉（高中）	NOI 2008 第一名；CMO 2009 第一名；CTSC 2011 / NOI 2011 命题委员会
学术兼职	中国计算机学会形式化方法专委会执行委员；TPChina 定理证明开放社区联合发起人
学术会议	CNCC 2022 论坛讲者；ChinaSoft 2023 论坛主席
教学课程	程序验证（ACM 班）、程序语言设计与实现（约翰·霍普克罗夫特班）、离散数学（荣誉）、人工智能前沿专题课
个人奖项	除上述外，公开资料未披露

七、Connection圈层总结

第一圈层：普林斯顿 Appel—VST 谱系。 导师 Andrew W. Appel 与 VST 项目构成其学术身份的内核：VST-Floyd、Verifiable C、VST-A 一脉相承，是该工具链从"验证研究"走向"可用工具"的关键推动力。Peter O'Hearn（分离逻辑工业化代表人物）的正面评价可视为该谱系在程序验证共同体中的背书。回国后他持续保持与普林斯顿方向的联系，VST-A 亦是在 VST 基础上的延伸。

第二圈层：北大哲学系逻辑学谱系。 王彦晶及北大逻辑学训练是其"哲学逻辑"底色的来源；这一圈层使其在"逻辑学—计算机科学"的跨学科地带（模态逻辑、认知逻辑、公开宣告逻辑）保持连接，也解释了其面向数学双学位的复合知识结构。

第三圈层：上海交大 JHC/人工智能学院网络。 与汪宇霆在程序语言方向形成 JHC 的"双支点"，与严骏驰、陈思衡等同事共同支撑学院研究生前沿课教学；在 AI 学院内，其"AI for 形式化验证"与"形式化方法 for AI 可靠性"的双向定位，与学院大模型与智能体主流方向形成互补性连接。

第四圈层：学生与后继网络（成型中）。博士生程章、硕士生吴基洋与 TOPLAS 2026 论文表明其学生培养已进入收获期；考虑到 2021–2025 年中国大陆以第一单位发表的 TOPLAS 论文仅 3 篇（据校方新闻），这一产出在国内程序语言领域属第一梯队。其"仅招收有相关背景学生"的高门槛招生策略，预示其学生网络将走"少而精"的证明工程路线。

SJTU-人工智能学院 曹钦翔 副教授