上交TCS 汪宇霆长聘教轨副教授

报告生成时间：2026年8月20日
个人主页：https://jhc.sjtu.edu.cn/~yutingwang/
所属团队：上海交通大学计算机科学与工程系 / 理论计算机科学研究所、约翰·霍普克罗夫特计算机科学中心

一、学者基本信息

字段	内容
姓名	汪宇霆（Yuting Wang）
职称	长聘教轨副教授
所属单位	上海交通大学电子信息与电气工程学院
所属研究所	理论计算机科学研究所、约翰·霍普克罗夫特计算机科学中心
学科	计算机软件与理论（081202）
电子邮件	yuting.wang@sjtu.edu.cn
研究方向	软件系统的形式化验证；程序设计语言；证明论与类型理论；逻辑框架；编译器验证；操作系统验证；Abella定理证明器开发

二、教育背景与职业履历

教育背景

时间	学校	专业	学位
2002.09 - 2006.07	上海交通大学	电力系统及其自动化	工学学士
2006.09 - 2009.02	上海交通大学	电力系统及其自动化	工学硕士
2009.09 - 2011.08	康涅狄格大学（University of Connecticut）	计算机软件与理论	理学硕士
2011.09 - 2016.12	明尼苏达大学双城分校（University of Minnesota, Twin Cities）	计算机软件与理论	理学博士

汪宇霆的学术经历颇为独特：他本科和硕士阶段在上海交通大学学习电力系统及其自动化，之后转向计算机科学领域。在康涅狄格大学获得计算机软件与理论硕士学位后，进入明尼苏达大学双城分校攻读博士，导师为Gopalan Nadathur教授。博士论文题为"A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs"（高阶抽象语法方法在函数式程序经验证编译中的应用）。

职业履历

时间	单位	职位
2017年至今（具体时间未公开）	上海交通大学约翰·霍普克罗夫特计算机科学中心	长聘教轨副教授
2016.12 博士毕业	明尼苏达大学双城分校	博士

三、学生培养情况

根据上海交通大学研究生院教师主页信息，汪宇霆已毕业3人，在读4人。从其论文发表记录中可以识别出的学生包括：

张玲（Ling Zhang）：参与多篇重要论文（POPL 2024、PLDI 2025），是汪宇霆团队的核心学生。
吴锦华（Jinhua Wu）：参与POPL 2024和APLAS 2023论文。
倪屹诚（Yicheng Ni）：参与APLAS 2024论文。
刘思宇（Siyu Liu）：参与TASE 2023论文。
徐向哲（Xiangzhe Xu）：参与CAV 2021论文。
宋一晨（Yichen Song）：参与APLAS 2023论文。

四、学术合作网络

4.1 所在团队内部合作

曹钦翔（长聘教轨副教授，约翰·霍普克罗夫特中心）：两人同为程序验证方向，在2024年同时各自有一篇论文被POPL 2024录用（汪宇霆的编译验证论文和曹钦翔的VST-A论文），虽然论文各自独立，但两人在同一研究所内形成了形式化方法方向的协同效应。
符鸿飞（副教授）：同属理论计算机科学研究所，研究方向有形式化方法的交叉。
傅育熙、龙环（并发理论方向）：虽同属研究所，但研究方向差异较大，直接合作较少。

4.2 跨机构合作

汪宇霆的跨机构合作网络以耶鲁大学为核心：

邵中（Zhong Shao）（耶鲁大学教授）：汪宇霆最重要的合作者。两人从POPL 2019开始持续合作，共同发表了多篇POPL和OOPSLA论文（POPL 2019、OOPSLA 2020、POPL 2022、POPL 2024、PLDI 2025、POPL 2025）。邵中是程序验证和编译器验证领域的国际权威，这段合作关系是汪宇霆学术网络的核心。
Jérémie Koenig：参与多篇与邵中合作的论文（POPL 2024、POPL 2025）。
Pierre Wilke：参与POPL 2019论文合作。
Gopalan Nadathur（明尼苏达大学教授）：汪宇霆的博士导师，在Abella定理证明器开发方面有深入合作。

4.3 国际合作

汪宇霆的国际合作网络非常突出，主要体现在：

耶鲁大学：与邵中教授的长期深度合作，形成了上海交通大学-耶鲁大学在编译器验证领域的联合研究团队。多项成果以上海交通大学为第一完成单位，耶鲁大学为合作单位。
明尼苏达大学：与博士导师Nadathur在Abella定理证明器方面的持续合作。
Kevin Chaudhuri：参与了汪宇霆早期论文（TLCA 2015、PPDP 2013）的合作。

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

汪宇霆的业界合作主要体现在与华为的合作：

CCF-华为胡杨林基金形式化专项项目（2023.10-2024.09）：项目名称为"Rust核心语言机制的编译验证方法"，这是一项直接面向Rust编程语言编译验证的应用导向研究。
基于Rust编译器验证的可组合内存安全研究（2025.01-2026.12）：延续Rust验证方向的研究项目。
面向LLBC增强语言的Rust编译和规约生成框架（2026.01-2027.01）：进一步拓展Rust验证的框架研究。

这三项华为联合基金表明，汪宇霆的编译验证研究已经与工业界的实际需求（特别是Rust语言的安全验证）紧密结合。Rust语言作为近年来最受关注的系统编程语言，其安全性的形式化验证具有重要的工业价值。

基于通用开放语义的可组合编译器验证研究（2024.01-2027.12）：国家自然科学基金项目，属于基础研究层面的编译器验证理论。

六、重要奖项与学术兼职

奖项

根据公开信息，汪宇霆的教师主页标注"获奖信息"暂无内容，但其在POPL这一程序设计语言领域最高级别会议上的连续发表本身就是学术实力的有力证明。

学术成果亮点

汪宇霆在程序设计语言顶级会议POPL上取得了令人瞩目的成绩：

年份	论文	会议
2019	An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code	POPL
2022	Verified Compilation of C Programs with a Nominal Memory Model	POPL
2024	Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules	POPL
2025	Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra	POPL
2025	CompCertOC: Verified Compositional Compilation of Multi-Threaded Programs with Shared Stacks	PLDI

此外还有OOPSLA 2020、CAV 2021、ESOP 2016、APLAS 2023/2024等多篇高水平论文。以上海交通大学为第一完成单位在POPL上连续发表4篇论文，在中国大陆高校中极为罕见。

学生培养

已毕业3人，在读4人（根据上海交通大学研究生院主页数据）。

七、Connection圈层总结

汪宇霆的学术关系网络呈现出"国际顶尖合作+本土成果产出"的鲜明特征：

核心圈层：以耶鲁大学邵中教授为核心合作伙伴的编译验证研究团队。这段从POPL 2019持续到POPL 2025的深度合作，是汪宇霆学术网络中最关键的合作关系，也是上海交通大学在POPL领域取得突破的重要推动力。

博士传承圈层：以明尼苏达大学Gopalan Nadathur教授为核心的Abella定理证明器开发社区。汪宇霆在博士阶段参与开发的Abella系统是其学术生涯的起点，这一传承在后续研究中持续发挥作用。

团队圈层：在上海交通大学理论计算机科学研究所内，汪宇霆负责"形式化验证——自动化验证"方向，与曹钦翔共同构成了形式化方法研究的双人核心。虽然两人在论文层面的直接合作较少，但在研究所内部形成了形式化方法方向的协同效应。

业界连接：通过CCF-华为胡杨林基金的项目合作，汪宇霆将其编译验证理论成功对接到Rust语言安全验证的工业需求中，形成了理论与实践的良性循环。这是理论计算机科学研究中较为成功的产学研结合案例。

学术特色与影响：汪宇霆的研究最突出的贡献在于将名义技术（Nominal Techniques）引入编译验证，提出了名义内存模型，开发了NominalCompCert、CompCertELF、CompCertOC等一系列CompCert扩展版本。这些工作在程序设计语言社区产生了重要影响，特别是在中国大陆高校，POPL连续发表的记录更是彰显了其研究的国际领先水平。

跨学科背景：从电力工程到计算机科学的跨学科转型，赋予了汪宇霆独特的视角，使其能够从系统层面的实际需求出发思考形式化验证问题。

发展阶段：汪宇霆正处于学术生涯的上升期，连续的POPL发表和华为合作项目表明其研究既有理论深度又有应用价值，未来发展潜力巨大。

上交TCS 汪宇霆 长聘教轨副教授