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 verification (software correctness), compilers and their applications for anything.

I took several gaps for industrial interns during my PhD study. I worked with the research team lead by Dr. Daniel Kröning at Amazon Web Services (AWS)s’ Automated Reasoning Group & Annapurna Labs, working on a formal verification of a realistic ML Compiler (AWS Neuron) using Lean 4 proof assistant.

I also worked with Pytorch & Triton development team at Meta Platforms, Inc., contributing to the open source Triton tensor language/compiler (built on LLVM/MLIR compiler framework) and provided new debugging support in connecting top Python AST and bottom CUDA PTX.

Before joining Georgia Tech, I spent my undergraduate time at Shanghai Jiao Tong University (SJTU), major in Computer Science and minor in Music. I was advised by Prof. Qinxiang Cao and worked on compiler correctness and mathematical logic in the Coq proof assistant (now renamed to Rocq) for Bachelor Thesis. Prior to that I studied in Prof. Xiang Yin’s’ group and worked on automata theory under control problems as my first academic research.

Here is my CV, LinkedIn, and Twitter.

Research

My current focus (PhD Thesis) is improving methods for compiler correctness in different angle, especially using formal verification through proof assistant. Whether for career or just for hobbies, 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 and I will share knowledge/ideas I have for free.

See the detailed open problems including other areas I’m investigating or interested below:

Formal Verification & Certified Compilation (Primary & Thesis Topic)

  • [GPU Compiler] [Ongoing] Compiler Correctness for Tensor Language

  • [CPU Compiler] [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] Verification for Realistic Tensor Compilers

  • Q: The compiler correctness is defined as “for any program, if the compiler accept it, the generated program always behaves the same (when source program behaves normal) or better (when source program will trigger error)”. However, how much can we reason about when the compiler reject a program? Such query is non-trivial, because a compilation pass that reject all program can be proved correct under CompCert’ s correctness setting.

  • Q: How can undefined behavior (UB) be exploit in a correct-by-construction compiler (e.g. CompCert) like what LLVM did?

  • 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? How far will it be from current general framework?

  • Q: How do we ensure what we proved correct is the correctness we want, i.e. that the formal semantics specification of C (source language) and assembly/machine language (target language) in CompCert is exactly 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.

  • General 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, keeping track of latest progress)

  • GPU Programming, CUDA, OpenMP, MLIR, etc.
  • Data-race problems
  • Program Verification with Concurrency: concurrent separation logic, etc.

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 (computability with human provided information)?

Undergraduate Research at SJTU

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

    I investigated the formal 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 using proof assistant. 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 Dr. 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, by Vivek Sarkar
    • The foundational principles of programming languages
  • Teaching Assistant for CS4510@GT: Automata and Complexity, 2022 fall, 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, 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, by Xiang Yin.
    • Deductive Logic, Graph Theory, Set Theory

Misc

  • My hometown is Chongqing, the Night City of China, a city built on mountains. Do pay a visit.

  • I’m a cat person. Here’s my cat.

  • I love tennis since high school, with skills around NTRP 3.5-4.0.

  • I sometimes play League of Legend (a MOBA Esport), while only ranking Platinum : (