介绍
本人现任上海交通大学长聘教轨副教授。之前在耶鲁大学计算机系有三年博士后经验(2016.12--2019.12),师从Zhong Shao。并于2016年从明尼苏达大学双城校区获得计算机系博士学位(2011.09--2016.12),师从Gopalan Nadathur。详细信息参见本人简历。
研究方向
本人主要研究如何利用程序语言理论和基于数学逻辑的证明方法提高软件可靠性。
具体方向如下:
本人目前主要研究系统软件的形式化验证技术和验证框架(例如,编译器和操作系统形式化验证)。本人还开发了验证关系式规约(Relational Specifications)的验证框架,该部分工作围绕着定理证明器Abella展开。
学生
-
研究生
-
倪亦澄 (博士研究生, 2024-)
-
吴进华 (博士研究生, 2022-)
-
张令 (博士研究生, 2021-)
-
刘思雨 (硕士研究生, 2021-)
主要开发及维护软件
-
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合作开发。
发表论文
(通讯作者标注为*)
-
Journal and Conference Papers
-
Ling Zhang, Yuting Wang*, Jinhua Wu, Jérémie Koenig, and Zhong Shao.
Fully Composable and Adequate Verified Compilation with
Direct Refinements between Open Modules.
Proceedings of the ACM on Programming Languages, 8(POPL), 2024.
[DOI
|PDF
|Slides
|Artifact
|TR
|Website]
-
Jinhua Wu, Yuting Wang*, Meng Sun, Xiangzhe Xu, and Yichen Song.
Towards a Framework for Developing Verified Assemblers for the
ELF Format.
The 21st Asian Symposium on Programming
Languages and Systems (APLAS), 2023.
[DOI
|Slides
|Artifact]
-
Siyu Liu and Yuting Wang*.
Verified Transformation of Continuation-Passing Style into Static Single Assignment Form.
The 17th International Symposium on Theoretical Aspects of Software Engineering (TASE), 2023.
[DOI
|Slides
|Artifact]
-
Yuting Wang, Ling Zhang, Zhong Shao, and Jérémie Koenig.
Verified Compilation of C Programs with a Nominal Memory Model.
Proceedings of the ACM on Programming Languages, 6(POPL), 2022.
[DOI
|PDF
|Slides
|Artifact
|Website]
-
Xiangzhe Xu, Jinhua Wu, Yuting Wang*, Zhenguo Yin, and Pengfei Li.
Automatic Generation and Validation of Instruction Encoders and Decoders.
The 33rd International Conference on Computer-Aided Verification (CAV), 2021.
[DOI
|Slides(short)
|Slides(full)
|Artifact]
-
Yuting Wang, Xiangzhe Xu, Pierre Wilke, and Zhong Shao.
CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files.
Proceedings of the ACM on Programming Languages, 4(OOPSLA), 2020.
[DOI
|PDF
|Slides]
-
Yuting Wang, Pierre Wilke, and Zhong Shao.
An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code.
Proceedings of the ACM on Programming Languages, 3(POPL), 2019.
[DOI
|PDF
|Slides
|Website]
-
Gopalan Nadathur and Yuting Wang.
Schematic Polymorphism in the Abella Proof Assistant.
Proceedings of the 20th International Symposium on Principles
and Practice of Declarative Programming (PPDP), 2018.
[DOI |
arXiv |
Slides |
Website]
-
Yuting Wang and Gopalan Nadathur*. A Higher-Order Abstract Syntax Approach
to Verified Transformations on Functional Programs.
The 25th European Symposium on Programming (ESOP), 2016.
[DOI |
arXiv |
Slides |
Website]
-
Yuting Wang and Kaustuv Chaudhuri. A Proof-theoretic Characterization of
Independence in Type Theory. The 13th International
Conference on Typed Lambda Calculi and Applications (TLCA), 2015.
[DOI |
Slides |
Website]
-
David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller,
Gopalan Nadathur, Alwen Tiu, and Yuting Wang. Abella: A System
for Reasoning about Relational Specifications. Journal of
Formalized Reasoning, 7(2), 2014.
[DOI]
-
Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, and Gopalan Nadathur.
Reasoning about Higher-Order Relational Specifications.
The 15th Symposium on Principles and Practice of Declarative Programming
(PPDP), 2013.
[arXiv |
DOI]
-
Yuting Wang and Gopalan Nadathur.
Towards Extracting Explicit Proofs from Totality Checking in Twelf.
The 8th ACM SIGPLAN International Workshop on Logical Frameworks
(LFMTP), 2013.
[arXiv |
DOI]
-
Che Guan, Peter Luh, Laurent Michel, Yuting Wang, and Peter Friedland.
Very Short-Term Load Forecasting:
Wavelet Neural Networks with Data Pre-Filtering.
IEEE Transactions on Power Systems, 28(1):30-41, 2013.
[DOI]
-
Ph.D. Thesis