Biography

My name is pronounced [Tzi-Teng Young]. I am a PhD student in the PLSE Group at Georgia Institute of Technology (GT) since 2021. I’m fortunate to be advised by Prof. Vivek Sarkar , John P. Imlay, Jr. Dean of the College of Computing. My current research interests are formal method (proof assistant, especially), compilers and their applications for anything.

News: I’m taking a small gap-year in tech company in 2025 for practical training on research and engineering around compiler technology and formal methods. I’ll take Applied Scientist Internship at Automated Reasoning Group at Amazon Web Services (AWS) starting Jan. 2025, lead by Dr. Daniel Kröning, working on a research project about formal correctness of ML Compilers .

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 for control problems during sophomore year.

I’m always open to general research collaboration. Feel free to reach out if you'd like to work on the problems I listed below or your ideas together.

Here is my CV.

Contact Information:

  • Email: (fun x y z =>x dot y dot z @gmail.com) cs ziteng yang
  • LinkedIn, Twitter

Research

My current major focus (PhD Thesis) is improving methods for compiler correctness in different angle, especially using formal verification through proof assistant. See the detailed problems including other areas I’m investigating or interested below:

Formal Verification & Certified Compilation (Primary & Thesis Topic)

  • [Ongoing] Improving the Correctness Theory of Certified Compiler: Investigating a “missing correctness specification” of CompCert framework through both testing and formal proofs.

  • [Ongoing] Verified Linear Scan Register Allocation: Implementing an alternative register allocation algorithm in a formally verified compiler instead of graph-coloring algorithm to reduce both compile-time complexity and verification burden.

  • [OOPSLA’24] [Improving] 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.

  • [Intern@Amazon] Correctness for ML Compilers

  • 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 to implement inter-procedural optimizations in a certified compiler? Is current general framework enough?

  • Q: How can undefined behavior (UB) be exploit in a certified compiler like LLVM did?

  • Q: How do we ensure that the formal semantics specification of C (source language) and assembly/machine language (target language) in CompCert is correct w.r.t. their language design?

    A: Testing the reference C interpreter (verified to follow the semantics) is all we need (existing work can be found). The assembly semantics is already proved to simulate the C semantics.

  • Q: Correct-by-construction verification using proof assistant guarantees total correctness but requires heavy proof work and much harder to scale, while translation validation of compiler passes like Alive2 is automatic, algorithm independent and works on real-world scenario, but only find false cases. Should we desire both advantages in one method?

Parallelism & Concurrency (secondary, trying to find good methods for important problems)

  • [Reading] Data-race problems: Investigating possible new approaches on both static prediction and dynamic detection of data-races.
  • [Reading] GPU Programming, Cuda, OpenMP, MLIR, etc.
  • [Reading] Program Verification with Concurrency: concurrent separation logic, etc.

General Theory (only in spare time, only for pleasure)

  • Computability view of Program Verification and Analysis: How do we establish a theory in computability view for certified programs annotated with its correctness information like Dafny, Viper, VST-A, etc. ? Can we conclude any non-trivial new theorems based on such model?

Undergraduate Research at SJTU

  • Compiler Correctness for Annotation Verifier [Corresponding author is Dr. Qinxiang Cao]:

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

    After I graduated, this expedition was continued by Hanzhi Liu, Yanning Chen, etc. to go beyond toy language using my framework. Expecting some publication(s) later.

  • [IFAC’20] Formal Control Theory (Automata Theory) [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 of an automata.

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 (10,000 CNY; 10 winners and 10 finalists among university each year) , 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…)