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 formal verification, proof assistant, compilers and their applications for anything.

Before joining Georgia Tech, I spent my undergraduate time at Shanghai Jiao Tong University (SJTU), major in Computer Science. I was advised by Prof. 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 Prof. Xiang Yin’s’ group and worked on automata theory (specifically, supervisory control of Discrete Event System) during sophomore year.

I’m open to internship and general research collaborations. Here is my CV.

Contact Information:

Research

My current major focus (PhD Thesis) is on improving certified compilation. In the meantime, I also pay attention to the area of parallelism & concurrency, general PL theory etc. See the detailed problems I’m investigating below:

Formal Verification (Proof Assistant) & Certified Compilation (Primary)

  • [Ongoing] Verified Linear Scan Register Allocation: Implementing an alternative register allocation algorithm in a formally verified compiler instead of graph-coloring algorithm that has both lightweight time complexity and verification burden.
  • [Ongoing] Improving the Correctness Theory of Certified Compiler: Investigating a “missing correctness specification” of CompCert framework.
  • [OOPSLA’24] Verified Instruction Scheduling: Achieved the first ever fully verified instruction scheduling passes in a formally verified compiler. Further exploration are into verified inter-block scheduling.
  • Q: How do we improve the general framework for CompCert to make a parallelizing compilation (e.g. Parallelizing loops in GCC -O3 optimization)
  • Q: How do we ensure that the formal semantics specification of C (source language) and assembly/machine language (target language) is correct w.r.t. their language design?
  • Q: How could equality saturation be used to improve a certified compiler optimization?
  • Q: How to implement inter-procedural optimizations in a certified compiler? Is current general framework enough?

Parallelism & Concurrency (secondary)

  • [Reading] Program Analysis on Data-race problems: Investigating some better approaches on both static prediction and dynamic detection of data-races.

General Theory (slowly, only in spare time)

  • Computability view of Program Verification and Analysis: How do we establish a theory in computability view for annotation verifier (programs annotated with its verification)?

Undergraduate Researches

  • Compiler Correctness for Annotation Verifier [Advised by Qinxiang Cao]:

    I worked on investigating correctness theory of compiling programs annotated with verification information (annotation verifier) and using them as optimization hints. I proposed an extended semantic and verification framework and gave a trial on toy language/logic.

    This expedition was continued by Hanzhi Liu, Yanning Chen, etc. to go beyond toy language using my framework.

  • Supervisor Control of Timed Discrete-Event Systems [Advised by Xiang Yin]: Investigated the supervisory control problem for timed discrete-event systems (TDES) under partial observation where time was considered as a special event.

Publications

Program Verification:

  • Ziteng Yang, Jun Shirako, and Vivek Sarkar. 2024. Fully Verified Instruction Scheduling. Proc. ACM Program. Lang. 8, OOPSLA2, Article 299 (October 2024), 26 pages.

    [ DOI l PDF l Slide ]

Automata Theory:

  • Ziteng Yang, Xiang Yin and Shaoyuan Li. “Maximally permissive supervisor control of timed discrete-event systems under partial observation,” in 21st IFAC World Congress, 2020.

    [ DOI l PDF l Slide l Video Report ]

Teaching Experience

  • Teaching Assistant for CS6390@GT: Programming Languages, 2023 spring, taught by Vivek Sarkar
    • The foundational principles of programming languages
  • Teaching Assistant for CS4510@GT: Automata and Complexity, 2022 fall, taught 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, taught 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, taught by Xiang Yin.
    • Logic and deduction, Graph Theory, Set Theory

Honors and Scholarships

During PhD Program

  • Conference Travel Grant by scholarship of PLMW@PLDI’22, San Diego, Jun. 2022

During Undergraduate Time

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

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

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

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

Misc

  • My hometown is Chongqing, the Night City of China. Do pay a visit.
  • I’m a cat person. Here’s my cat.
  • I love tennis. (But it hurt my bone…)