About

I am a PhD student in the PLSE Lab at Georgia Institute of Technology (GT) since 2021, advised by Prof. Vivek Sarkar.

My current research interests lies in Programming Languages (PL) and Formal Methods.

Here is my CV.

Contact Information:

Biography

During my undergraduate time at Shanghai Jiao Tong University (SJTU), major in Computer Science and Technology , I was advised by Qinxiang Cao and worked on compiler correctness and mathematical logic in the Coq proof assistant from junior to senior year . Prior to that I studied in Xiang Yin’s group and worked on Automata Theory (specifically, supervisory control of Discrete Event System) during sophomore year. They are the persons who taught me a huge number of things during undergraduate life and gave me a great start of research life.

Research Projects

During PhD Time

I will probably investigate a subset of researches around those general topics in the following two years:

  • [actively working on] Program analysis for parallel programs ;
  • Combining static analysis and formal verification;
    • Formally verified static analysis
    • Static analysis with extra information from formal verification
  • Program verification for concurrent program;

During Undergraduate Time

  • [2020~2021, Compiler Verification] Verification-aided Compiler Optimization

    • This is an expedition to support compiler optimization aided by verification information carried by programs;
    • I proposed a verification framework based on proof assistant Coq and gave a trial on “toy logic”;
    • This project was now continued by Hanzhi Liu to implement this optimization and framework in VST’s Separation Logic [VST := Verified Software Toolchain]; further detail should be secret now; there should be a paper submission soon
  • [2019~2020, Proof Assistant & Mathematical Logic] Finite Canonical Model for Completeness Theory in Coq Based on UnifySL: An extension from framework of infinite model for completeness theorem proof to finite model in a logic library UnifySL for Coq proof assistant.
  • [2018~2019, Formal Control Theory] Supervisor Control of Timed Discrete-Event Systems: Investigating the supervisory control problem for timed discrete-event systems (TDES) under partial observation where time was considered as a special event.

Publications

During PhD Program

There should be some years later …

During Undergraduate Time

Program Verification:

  • [There might be one later (submitted to OOPSLA 2022)]

Formal Control Theory:

  • Ziteng Yang, X. Yin and S. Li. “Maximally permissive supervisor control of timed discrete-event systems under partial observation,” in 21st IFAC World Congress, 2020. [ Conference Paper l PDF l Slide l Video Report (Youtube) ].

Teaching Experience

  • Teaching Assistant for MA208@SJTU: Discrete Mathematics, 2020 fall, lectured by Qinxiang Cao .
    • Courses for the IEEE Honor Class & Artificial Intelligence Class at SJTU
  • Teaching Assistant for MA239@SJTU: Discrete Mathematics (Honor), 2020 fall, lectured by Xiang Yin.

Honors and Awards

During PhD Program

Wish I could have some in the future : )

During/Before Undergraduate Time

  • Rongchang Scholarship for Science and Technology Innovation, Finalist (30 persons school-wide each academic year; 10,000 CNY) , Oct. 2020

    荣昶科技创新奖学金, 提名奖 (人民币壹万元)

  • Undergraduate Excellent Scholarship, Third-class (Top 20%; 500 CNY), Oct. 2018

    上海交通大学校优奖学金, C等 (人民币伍佰元)

  • 1st Prize in National High School Mathematics League in Provinces, Sept. 2016

Projects for Courses/Fun

See more details in Projects .