Yuting Wang

Associate Professor (tenure-track)
John Hopcroft Center for Computer Science
Shanghai Jiao Tong University
Research Interests

My research interests are broadly in the area of formal verification of software systems. Within this context, I am interested in developing specification and reasoning formalisms, in constructing systems that implement these formalisms and in applying the formalisms using the systems that implement them to verify software artifacts

Selected Publications
  • Ph.D. Thesis

  • Conference Papers

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

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

© John Hopcroft Center for Computer Science, Shanghai Jiao Tong University

邮箱:jhc@sjtu.edu.cn 电话:021-54740299