About

I am a first-year PhD student in the PLSE Lab at School of Computer Science, College of Computing, Georgia Institute of Technology (GT).

My research experience lies in Programming Languages (PL) and Formal Methods. PhD program is a brand new stage of my life. I’m still exploring the various researches in PL.

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 Modal Logic in 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.

Here is my CV.

Contact Information:

Research Projects

During PhD Program

To be updated soon (or maybe a year later)

I will probably investigate a subset of researches around those general topics in the following one or two years:

  • Program analysis for parallel programs [actively working on];
  • Graph reachability problems and their application with static analysis [actively working on];
  • Program synthesis and computability problems related to them;
  • Software testing (generally);
  • Combining static analysis and formal verification;
  • Program verification for concurrent program;

If you found that we shared similar interests, I’d be excited to have a cheerful discuss with you!

I will probably also be learning the fundamental knowledges of those topics in the following one or two years:

  • Computability
  • Separation Logic (both meta-theory and application),
  • Meta-theory of Coq proof assistant, i.e. Calculus of Constructions
  • Basic knowledge of type theory
  • LLVM

During Undergraduate Time

  • [2020~2021] Verification-aided Compiler Optimization
    • I proposed a frame verification work based on proof assistant Coq and gave a trial on “toy logic” for an expedition to support compiler optimization aided by verification information carried by programs
    • This project was now continued by Hanzhi Liu, an undergraduate genius student (2019~2023, expected) and an experienced programmer at SJTU, also advised by Qinxiang Cao, 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] 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] 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.

Publication

During PhD Program

To be updated in the future

  • If there’s still nothing several years later, either of the two things might happened: 0- I have forgotten I have a personal website; 1- : (

During Undergraduate Time

Program Verification:

  • There might be one later …

Formal Control Theory:

  • 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. [ 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 (an honor class for elite students in EECS) & 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 (a program only for top 5% students in Engineering related majors) 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 school-wide each academic year; 10,000 CNY) , Oct. 2020

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

  • Undergraduate Excellent Scholarship, Third-class (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 .

Useful Links For CS Study

Some Professors’ Website

Programming Languages & Formal Methods in Computer Science

Materials for CS Study from Internet

Stock up maybe-useful resources like the hamster …

a. Programming Languages (Research Oriented)

Program Analysis

Program Verification

b. Theoretical Computer Science (Interests Oriented)

  • Prof. Ryan O’Donnell at CMU keeps uploading videos about basic theoretical computer science in YouTube and Bilibili

    卡内基梅隆大学的 Ryan O’Donnell 教授一直在 YouTuBe 和 B站 上传理论计算机相关的科普视频

c. Computer System (Courses Oriented)

**$\alpha$ Tools **

Miscellany

Sentences I wish to share

[Inside Chinese internet, we some times called it “chicken soup” if some sentence or story is heuristic]

  • “Talk is cheap. Show me the code.” — Linus Torvalds

  • “Talk is cheap. Show me the proof.” — Qinxiang Cao

  • “Talk is not cheap” — Some Cyber-stranger

  • “闻道有先后，术业有专攻” — 韩愈

    One might have learned the doctrine earlier than the other, or might be a master in his own special field. — Yu Han

  • Russell’s Message:

    • “Ask yourself only what are the facts and what is the truth that the facts bear out”

    • “Never let yourself be diverted either by what you wish to believe or by what you think would have beneficent social effects if it were believed, but look only and solely at what are the facts.”

    • “Love is wise, hatred is foolish.”

Current Future Plans

  • Learn more things in Logics, Mathematics and Computer Science (especially in PL, Theory and System);
  • Raise a cat in 2 years (I will immediately raise one after passing my qualification examination, sincerely.)

Entertainment

What I am exited about during leisure time:

  • Sports: Tennis = badminton > volleyball » table tennis
  • Animals (I do not have any pets…): cats, dogs, hamsters, … (I really like this couple’s video 强烈推荐up主 九品芝麻铲屎官 的视频剪辑)
  • Movies:
    • Interstellar (星际穿越) (the foremost one) [now you might know why I sometimes use “Intelstealer” as a nickname …] [YouTube, Bilibili]
    • The Dark Knight (黑暗骑士) [YouTube, Bilibili]
    • Big Fish (大鱼) [YouTube, Bilibili]
    • Life in a Day (a movie consistent of clips from all over the world in the same ordinary day made by Youtube)
    • 钢的琴 (The Piano in a Factory) [Bilibili]
    • Before Sunrise (爱在黎明破晓前) [YouTube, Bilibili]
    • The Last Emperor (末代皇帝) [Bilibili]
    • World War Z (A good zombie movie; I like the design of its foreshadowing) [YouTube, Bilibili]
    • Mad Max: Fury Road (I like the design of the post-apocalyptic world)
    • 无人区 (No Man’s Land)
    • Movies from Marvel Cinematic Universe and DC Extended Universe

  • TV series: recalling …

  • Games:
    • Red Dead Redemption 2 (the favorite one)
    • Life is Strange
    • Plants VS. Zombies, Plant VS. Zombies 2
    • Cytus II, Deemo, Lanota (all are music games)
  • Instruments: Harmonica, (Piano, 10 years ago I can play it; now I can only love it)
  • Music and Favorite Singers/bands:
    • Pop Music Singers/bands I was addicted to:
      • Around 2019 ~ Now: Li Chen (95% of her albums and singles) and Nightwish (Imaginaerum, Dark Passion Play and Endless Forms Most Beautiful )
        • Have a taste: Updating …
      • Around 2015 ~ 2018: Ellie Goulding (98% of her albums and singles) and Bea Miller (Fire N Gold, etc.)
        • Have a taste: Updating …
      • Around 2012 ~ 2015: Britney Spears and Kesha
      • Around 2011: Jay Chou, Michael Jackson, Song Xu, etc.
    • Classical Music (I was not an expert. In fact, I know nothing but just enjoy it.) :
      • Sonata No.8 in C Minor, Op.13, “Pathétique”, I, II and III
      • Sonata No.14 in C-Sharp Minor, Op. 27 No.2, “Moonlight”, I , II and III
      • Symphony No. 9 in E minor, Op. 95 “From the New World”: IV. Allegro con fuoco
      • Fantaisie-Impromptu in C-Sharp Minor, Op. posth. 66
      • Nocturne No.2 in E Flat Major, Op.9, No.2
      • Serenade by Schubert
      • VI. Waltz 2 from Jazz Suite No.2
      • Canon in D major by Pachelbel
      • “Modlitwa dziewicy” Op. 4 (A Maiden’s Prayer)
      • Concerto No. 1 in E major, Op. 8, RV 269, “Spring”
      • Habanera from Carmen
      • Swan Lake, Op. 20a: No.1
    • Traditional Chinese Music:

    • Related to politics/patriotism (I hate politics, but I love music):

      • 我的祖国 (My Homeland) [ YouTube: original version from 1956; a symphonic version ]

        This is a song that almost every one who came from China’s mainland can sing

      • 钢铁洪流进行曲 (March of Steel Torrent) [YouTube]

        This is a new Chinese Military Song written in 2019

      • La Marseillaise (the national anthem of France; 中文译名马赛曲，法国国歌) [YouTube]

      • Катюша (Katyusha, 喀秋莎)

      • Soviet March (A joke song written by a US composer 苏维埃进行曲，美国作曲家编写的嘲讽苏联的歌曲😅) : D

    • From Movies & Games: updating
      • Interstellar:
      • Plant VS Zombies:
      • Plant VS Zombies 2:
      • Red Dead Redemption 2:
      • Life is Strange
      • Cytus II & Deemo
      • Les Misérables: Look Down, At The End of The Day, The Docks (Lovely Ladies), The Confrontation, Castle on a Cloud, Master of the House, Do You Hear The People Sing
      • La La Land:
      • Coco: Remember Me, Proud Corazón
      • The Hanger Games:
      • Sherlock Holmes:
      • Suicide Squad:
      • デジモンアドベンチャー (Digimon Adventure): 勝利〜善のテーマ〜, Butterfly, Brave Heart
      • ウルトラマンティガ (Ultraman Tiga):
      • Attack on Titan:
      • Game of Thrones:
    • Other songs I was addicted to and wish to share (categorized by language):
      • [Chinese] 千千厥歌 (Thousands of Songs), 认真地老去, 杀死那个石家庄人, 黑色也是值得被等待的, 夜的第七章 , 下一站茶山刘, 月牙湾, 华阴老腔一声喊, 万物生
      • [English] Five Hundred Miles, Hotel California, The Sound of Silence, Hedwig’s Theme, New Year’s Eve, Wake Me Up, Waiting For Love, Sparks Fly, …
      • [Japanese] 手紙〜拝啓 十五の君へ〜, 夢灯籠, ぜんぜんぜんせ, PLANET
      • [Russian] Катюша (Katyusha), Skoro dembel’, Подмосковные Вечера (Moscow Nights)
      • [Piano] 翘课 (skip class), Flower Dance, 风の住む街, 城南花已开
      • [Violin]
      • [Accordion]
      • [Computer Generated] BASARA
      • updating
    • Interesting songs (好玩的):

Some Cyber-friends :)

  • I am fortunate to know Ziteng Wang, who share the same spell of first name, similar spell of last name, and most importantly, the research interests in Programming Languages with me.
  • I shared a similar game interest with Zhiming Xu, although we seem not to share similar research interests
  • Alex Chi is an undergraduate student (graduate at 2022) from the department of Computer Science at SJTU; you might be interested in his (famous, somehow) programming skills and (famous, somehow) course grades
  • xxchan used to be in the same research group with me during undergraduate time. His experience (see this blog) in an company might be a great reference for those (in China) who are still not sure whether going academical or industrial.

Cooking

To be updated when I became a master of that …

Share Some Facts

“The Joke’s On Me” - Jokes in My Real Life

  • I usually mix up with “sophomore” and “semaphore” (This happens for at least 5 times …)
  • The first day I arrived at my undergraduate college, I need to configure the internet in my dormitory. Since I had never got in touch any concept about computer system yet, when they asked me to provide the MAC address, I mistook for that I must have a Mac from apple to earn the accessibility to the Internet.
  • …

Jokes/Meme (all from internet)

  • image-20210923044320769

  • “WHAT IS YOUR ADDRESS”

    image-20210921223916342

  • “GIT PUSH”

    图像

  • “TO BE OR NOT TO BE”

    image-20210923033055472

  • “QED.”

    image-20210923034530903

  • “IT WORKS”

    image-20210923034746198

    image-20210923040119431

  • “WHO CARES”

    image-20210923034833337

  • “VAN GOGHS”

    image-20210923035144252

  • image-20210923035244315

  • image-20210923035355800

  • image-20210923035812923

  • …

Computer Science in My Life

  • I was also admitted by the Master of Logic program at the University of Amsterdam. But not rich enough to enroll : ( [It requires around 10,000 for tuition and another 10,000 or maybe more for life expenses …]
    • It doesn’t mean I do not love Computer Science; they are somehow mutually inductive magics of the world
  • I gave up the desire of stepping into game design, another totally different career life at sophomore. This is mainly because I didn’t found neither a good mentor/advisor nor ideal partners and didn’t make it by self-study.
    • It doesn’t mean I do not love Programming Languages. Instead, I found those two things in the area of Programming Languages later!
    • Nevertheless, I always love the world of video games and believe they are a treasure of humans.
  • I have no industrial experience till now. I still regard myself as a very nonprofessional programmer…
  • Unlike a lot of my friends that started learning programming at a very young age, I never touched the world of computer science until freshman year at SJTU.

Life

  • I was born and raised up in Chongqing, China. This is a magical city built on several mountains. You should pay a visit if you’d like to see how such thing could exist. Besides, my father comes from Hebei Province in China and worked there in a small city named Zhuozhou for a very long time, which is only 1-hour-drive to Beijing . Therefore, I was also familiar with those cities.
  • Although I lived in Shanghai for 4 years during my undergraduate life, I know nothing about Shanghai at all because I spend most of my time on campus : ( The fact is, you will spend even less (a half) time to go to the downtown area in Shanghai from Hangzhou, Zhejiang Province than going there from Shanghai Jiao Tong University.
  • …