Yuting Wang (in Chinese: 汪宇霆)

John Hopcroft Center for Computer Science Shanghai Jiao Tong University Room 201, IEEE Building No.1, No.800 Dongchuan Road, Minhang District Shanghai 200240, China Email: <first name>.<last name> at sjtu.edu.cn https://orcid.org/0000-0003-3990-2418 DBLP Google Scholar

!!2025研究生招募!!

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

• Rust编译器验证和开发
• 基于形式化验证的可信编译器后端（类LLVM后端）
• 安全程序语言设计和实现（程序构造开始直接排除内存安全和资源安全漏洞）
• 基于安全编程语言的系统软件开发
• 并发函数式编译器验证
• 其他课题或自选课题

About Me

I am currently a Tenure-Track Associate Professor at Shanghai Jiao Tong University. Before that, I was a postdoctoral researcher at Yale University supervised by Zhong Shao from December 2016 to December 2019. I obtained my Ph.D. degree at the University of Minnesota, Twin Cities under the advisory of Gopalan Nadathur. More detailed information can be found in my curriculum vitae.

Research Interests

I am broadly interested in the following research areas:

• Formal Verification
• Programming Languages
• Proof Theory and Type Theory
• Logical Framework

My current research focuses on techniques and frameworks for verifying system software (including compilers and operating systems). I am also involved in developing theories and frameworks for programming, specifying and verifying rule-based relational specifications. This line of research centers on the development of the Abella theorem prover.

Upcoming Events

• Introduction to Functional Programming
• Study of Compiler Verification
• Seminar on the Foundations for Programming Languages

Students

• Current

  • Yizhou Mao (Ph.D., 2025-)
  • Yicheng Ni (Ph.D., 2024-)
  • Jinhua Wu (Ph.D., 2022-)
  • Ling Zhang (Ph.D., 2021-)
  • Dongwen Yao (M.S., 2024-)

Alumni

• Siyu Liu (M.S., 2021-2024), Tencent
• Xiangzhe Xu (Undergraduate Intern, 2020-2021), Ph.D. student at Purdue University
• Zhenguo Yin (Graduate Intern, 2020-2021), AMD

• Prospective Students

  I am always looking for self-motivated undergraduate, master and Ph.D. students to collaborate with. If you are interested in or around my research areas, feel free to contact me.

Software

• Abella (http://abella-prover.org)

  I am one of the core developers of the Abella theorem prover since 2013. Abella is an interactive theorem-prover that is noteworthy for its support of higher-order abstract syntax and for the two-level logic approach to reasoning about formal specifications. This system represents joint work with other researchers at the University of Minnesota and at INRIA, Saclay, France. My contributions to the system were to build a complete treatment of an expressive specification logic called the logic of higher-order hereditary Harrop formulas, to co-develop a methodology for using this enhancement in complex reasoning tasks (collaboration with Kaustuv Chaudhuri) and to co-design and implement a form of polymorphism called schematic polymorphism to support polymorphic reasoning (collaboration with Gopalan Nadathur).




• Stack-Aware CompCert (https://certikos.github.io/compcertmc/)

  The state-of-the-art verified compiler for C is CompCert, whose verified compilation chain outputs abstract assembly code in Coq. Further compilation to machine code is handled by an unverified external toolchain. Collaborating with Pierre Wilke and Zhong Shao, I designed and implemented an extension to CompCert that supports verified compilation to machine code. The key idea is to instrument the memory model of CompCert with an explicit notion of stack (hence making CompCert “Stack-Aware”), so that the stack consumption is preserved by compilation. This enables a finite stack in CompCert that, together with the finite code and data, can be mapped to the finite memory space on real machines. Stack-Aware CompCert also supports a form of compositional compilation known as contextual compilation for composing verified abstraction layers. Contextual compilation provides the basis for compositionality of kernel modules in the verified operating system CertiKOS.

Publications

(Corresponding authors are marked with *)

• Journal and Conference Papers

  • Yu Zhang, Jérémie Koenig, Zhong Shao, and Yuting Wang. Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra. Accepted to POPL 2025.
  • Yicheng Ni, Yuting Wang^*. Generic Reasoning of the Locally Nameless Representation. The 22nd Asian Symposium on Programming Languages and Systems (APLAS), 2024. [DOI |Slides |Artifact]
  • 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

  • Yuting Wang. A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs. [arXiv | Pdf (with fixes after submission)]