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 interests 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 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
Here is my CV.
Contact Information:
 Email Address (Institution): (fun x y => x dot y @gatech.edu) firstname lastname
 Physical Address:
0CDD24F6DE9CKlaus Advanced Computing Building, room 2319  GitHub, Twitter
Research
Currently
 Program Logic & Certified Compilation (e.g. improving CompCert, computability aspect of verification)
 Parallel programs (e.g. verification of parallelizing compilers, analysis of parallel program)
During Undergraduate Time
 [2020~2021, Compiler Verification] Verificationaided 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 DiscreteEvent Systems: Investigating the supervisory control problem for timed discreteevent 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; cofirst 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 coworkers ; Cao is our advisor. ]
Formal Control Theory:
 Ziteng Yang, X. Yin and S. Li. “Maximally permissive supervisor control of timed discreteevent 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, contextfree language and PDA, Turning Machine, P/NP/coNP., L/NL, coNL

Teaching Assistant for MA208@SJTU: Discrete Mathematics, 2020 fall, lectured by Qinxiang Cao .
 Firstorder Logic (proof, semantics and soundness), Set Theory and Foundation of Mathematics

Teaching Assistant for MA239@SJTU: Discrete Mathematics (Honor), 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 schoolwide each year; 10,000 CNY) , Oct. 2020
荣昶科技创新奖学金, 提名奖 (人民币壹万元)

Undergraduate Excellent Scholarship, Thirdclass (Top 20%; 500 CNY), Oct. 2018
上海交通大学校优奖学金, C等 (人民币伍佰元)

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