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:

Email Address (Institution): ziteng.yang@gatech.edu

Physical Address:
0CDD24F6DE9CKlaus Advanced Computing Building, room 2319
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] 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 might be one later (submitted to OOPSLA 2022)]
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 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.
 Courses for the Zhiyuan Honor Program at SJTU;
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 academic 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
Projects for Courses/Fun
See more details in Projects .