上海交通大学 约翰·霍普克罗夫特计算机科学中心 电信群楼1-203室, 上海市闵行区东川路800号,200240 电子邮箱: <first name>.<last name> at sjtu.edu.cn |
本人将招募2025年入学的硕士及博士研究生。如果你有良好的学术背景,并对程序语言和形式化方法方向有兴趣(参见本研究组海报),请与我联系。可能研究项目包括:
本人现任上海交通大学长聘教轨副教授。之前在耶鲁大学计算机系有三年博士后经验(2016.12--2019.12),师从Zhong Shao。并于2016年从明尼苏达大学双城校区获得计算机系博士学位(2011.09--2016.12),师从Gopalan Nadathur。详细信息参见本人简历。
本人主要研究如何利用程序语言理论和基于数学逻辑的证明方法提高软件可靠性。 具体方向如下:
本人目前主要研究系统软件的形式化验证技术和验证框架(例如,编译器和操作系统形式化验证)。本人还开发了验证关系式规约(Relational Specifications)的验证框架,该部分工作围绕着定理证明器Abella展开。
Abella是明尼苏达大学和法国国家信息与自动化研究所(INRIA)联合开发的基于高阶抽象语法(Higher-order Abstract Syntax)的逻辑证明框架。其特点是支持复杂的高阶语言和逻辑系统的形式化建模及验证,已被成功应用于多种程序语言的形式化设计、程序语言基础理论的验证、以及函数式编译器验证。本人从2013年起作为Abella开发和维护的核心团队成员,负责其基础理论研究、验证方法设计、以及这些方法的实现。主要研究成果包括在Abella 2.0.0版本中加入对高阶关系式规约的支持(与INRIA研究员Kaustuv Chaudhuri的合作成果)以及加入对多态验证的支持(与Gopalan Nadathur的合作成果)。
CompCert作为应用最为广泛的经形式化验证的C语言编译器,其目标语言为一种抽象的汇编语言。从该汇编语言到机器代码的编译过程依赖于未经验证的外部工具(如GNU汇编器)。Stack-Aware CompCert 通过扩展CompCert实现了从源程序到机器代码完整编译过程的验证。其关键创新点如下:通过扩展CompCert的内存模型使其支持明确的栈结构,以证明程序的栈空间消耗能被编译过程保存,最终将栈空间和数据及代码段映射进入实际机器语言支持的有限内存模型。通过上述扩展,Stack-Aware CompCert实现了从CompCert汇编到机器代码的验证,并结合CompCert实现了从C程序到机器代码的端到端编译过程的验证。Stack-Aware CompCert同时还提供了一种名为Contextual Compilation的模块化编译和验证方法,为经验证的操作系统内核CertiKOS提供了编译验证的基础。Stack-Aware CompCert由本人与Pierre Wilke和Zhong Shao合作开发。
(通讯作者标注为*)