About & Biography

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 area are Programming Languages (PL) , specifically, program logic & verification, parallelism&concurrency, and their application in compiler.

Before joining Georgia Tech, I spent my undergraduate time at Shanghai Jiao Tong University (SJTU), major in Computer Science and Technology. I worked as a research assistant 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.

Here is my CV.

Contact Information:

Research

Currently

  • Program Logic & Certified Compilation (e.g. improving CompCert, computability aspect of verification)
  • Parallelism & Concurrency (e.g. verification of parallelizing compilers, prediction of data-race)

During Undergraduate Time

  • [2020~2021, Compiler Verification] Verification-aided Compiler Optimization
    • Project to support certified compiler optimization aided by verification information as a hint 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 should might be one later; co-first author; I designed the theory framework and implemented it as a general framework in Coq; the implementation based on a concrete separation logic are done by my co-workers ; Cao is our advisor. ]

Automata 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 CS4510@GeorgiaTech: Automata and Complexity, 2022 fall, lectured by Joseph Jaeger
    • Intro to Compatibility: regular language and DFA/NFA, context-free language and PDA, Turning Machine, P/NP/co-NP., L/NL, co-NL
  • Teaching Assistant for MA208@SJTU: Discrete Mathematics (IEEE/AI Honor Class), 2020 fall, lectured by Qinxiang Cao .
  • First-order Logic (proof, semantics and soundness), Set Theory as foundation of Mathematics
  • Teaching Assistant for MA239@SJTU: Discrete Mathematics (Zhiyuan Honor Class), 2020 fall, lectured by Xiang Yin.
  • Logic and deduction, Graph Theory, Set Theory

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