汪宇霆


上海交通大学
约翰·霍普克罗夫特计算机科学中心
电信群楼1-203室, 上海市闵行区东川路800号,200240

电子邮箱: <first name>.<last name> at sjtu.edu.cn

DBLP

Google Scholar

English Website

!!2025研究生招募!!

本人将招募2025年入学的硕士及博士研究生。如果你有良好的学术背景,并对程序语言和形式化方法方向有兴趣(参见本研究组海报),请与我联系。可能研究项目包括:

介绍

本人现任上海交通大学长聘教轨副教授。之前在耶鲁大学计算机系有三年博士后经验(2016.12--2019.12),师从Zhong Shao。并于2016年从明尼苏达大学双城校区获得计算机系博士学位(2011.09--2016.12),师从Gopalan Nadathur。详细信息参见本人简历

研究方向

本人主要研究如何利用程序语言理论和基于数学逻辑的证明方法提高软件可靠性。 具体方向如下:

本人目前主要研究系统软件的形式化验证技术和验证框架(例如,编译器和操作系统形式化验证)。本人还开发了验证关系式规约(Relational Specifications)的验证框架,该部分工作围绕着定理证明器Abella展开。

当前活动

学生

主要开发及维护软件

发表论文

(通讯作者标注为*)