[ News: I will join Georgia Institute of Technology as a PhD student in Computer Science at fall 2021 ! ]

My current research experience lies in Programming Languages and Formal Methods. I also have a short research experience in Automata Theory.

During my undergraduate time at Shanghai Jiao Tong University, major in Computer Science and Technology , I was advised by Qinxiang Cao and worked on compiler correctness and Modal Logic in Coq proof assistant from junior to senior year . Prior to that I studied in Xiang Yin’s group and worked on 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.

Here is my CV.


Research Projects

The following lists my most important research experiences during undergraduate study.

See more details in Projects .


  • Verification-aided Compiler Optimization: An expedition to support compiler optimization aided by verification information carried by programs


  • 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.

  • 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.


Conference Paper:

  • 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.

    [ PDF l Slide l Video Report (Youtube) ].

Teaching Experience

  • Teaching Assistant (unofficial) for MA208@SJTU: Discrete Mathematics, 2020 fall, lectured by Qinxiang Cao .
    • Courses for the *IEEE Honor Class (an honor class for elite students in EECS) at SJTU & Artificial Intelligence Class *
    • Duties: Q&A, making answer sheets for exercises
  • Teaching Assistant (official) for MA239@SJTU: Discrete Mathematics (Honor), 2020 fall, lectured by Xiang Yin.
    • Courses for the Zhiyuan Honor Program (a program only for top 5% students in Engineering related majors) at SJTU;
    • Duties: exercise grading, tutorials (for exercises) teaching, office hours holding and Q&A

Other Projects

The following projects are selected either from course work or my entertainment during spare time:

  • SimPL Interpreter: an interpreter for a simple programming language called SimPL, implemented in 2020.

  • Naive-Airdrop: an application for encrypted file synchronization between PC and Android under the same wi-fi, implemented in 2019.

    (Both my first project using Java and first practical project for real life.)

  • Re-implementation of deque and map of C++ Standard Template Library (STL): Re-implement the data structure deque (using Block List) and map (using AVL Tree) of C++ Standard Library, simulating most of their original designed functions, implemented in 2018.

    (My first project of programming.)

See more details in Projects .

Honors and Awards

  • Rongchang Scholarship for Science and Technology Innovation, Finalist (30 persons school-wide each academic year; 10,000 CNY) , Oct. 2020
  • Undergraduate Excellent Scholarship, Third-class (Top 20%; 500 CNY), Oct. 2018
  • 1st Prize in National High School Mathematics League in Provinces, Sept. 2016


Sentences I wish to follow

  • “Talk is cheap. Show me the code.” — Linus Torvalds
  • “闻道有先后,术业有专攻” — 韩愈

Current Future Plans

  • Learn more things in Logics, Mathematics and Computer Science (especially System and Theory);
  • Raise a cat in 2 years.


  • Sports: Tennis, badminton, volleyball, table tennis
  • Instruments: Harmonica
  • Movies: Interstellar (the favorite one), The Dark Knight, movies from Marvel Cinematic Universe and DC Extended Universe, etc.
  • Games: Red Dead Redemption 2 (the favorite one), Life is Strange, Plants VS. Zombies.