中文主页

About Me

I am currently a Tenure-Tracked Associate Professor at Shanghai Jiao Tong University. Beofre 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 actively 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. For a more comprehensive introduction to my research, please consult my research statement.

Upcoming Events

• Study of Compiler Verification

Prospective Students

I am currently 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

• Ph.D. Thesis

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

• Conference Papers

  • Yuting Wang, Xiangzhe Xu, Pierre Wilke, Zhong Shao. CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files. The 2020 ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2020. [DOI |PDF]
  • Yuting Wang, Pierre Wilke, Zhong Shao. An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code. The 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2019. [DOI |PDF |Slides |Website]
  • Gopalan Nadathur, 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, 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, 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]
  • 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]

• Journal Papers

  • 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]
  • 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]

• Workshop Papers

  • 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]