Litao Zhou (Tony)

Litao Zhou (Tony)

Senior undegraduate

Shanghai Jiao Tong University

Biography

Hi, this is Tony, a senior Computer Science student in Shanghai Jiao Tong University. I will be joining HKU PL Group in 2022 Fall. I am interested in programming languages and verification, especially areas where mechanical proofs are applied. I have experience with Coq, VST, and Abella theorem provers.

Download my resumé.

Interests
  • Formal Verification
  • Programming Languages
  • Type Systems
Education
  • Non-Graduating Exchange Student, 2021 Fall

    National University of Singapore (School of Computing)

  • BSc in Computer Science (IEEE Pilot Class), 2018-2022(Expected)

    Shanghai Jiao Tong University

Experience

 
 
 
 
 
Research Assistant (Part-time)
Dec 2021 – Present The University of Hong Kong, Remote
Studying iso-recursive subtyping.
 
 
 
 
 
Research Intern
Jul 2021 – Dec 2021 National University of Singapore, Singapore
Automatic Verification of Higher Order Programs (One-semester personal project).
 
 
 
 
 
Final Year Project
May 2021 – Present Shanghai Jiao Tong University, Shanghai
VST-A, a control-flow splitting system for formal verification of assertion-annotated C programs.
 
 
 
 
 
Software Engineer Intern
Sep 2020 – Jan 2021 Shanghai
In Visual and Parallel Computing Group, developed a web-based automation tool to smooth the testing workflow of graphics drivers.
 
 
 
 
 
Research Intern
Jul 2020 – Aug 2021 Shanghai Jiao Tong University, Shanghai
Formal verification of functional programming compilers in Abella.
 
 
 
 
 
Research Intern
Jan 2019 – Present Shanghai Jiao Tong University, Shanghai
Graph algorithm verification in Coq and VST.