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:
0C-DD-24-F6-DE-9CKlaus 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] 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 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. ]
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 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, 2020 fall, lectured by Qinxiang Cao .
- First-order 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 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