Ruotong Cheng
I am a third-year Ph.D. student in the PLSE group at the University of Toronto. My advisor is Prof. Azadeh Farzan. My research area is formal methods, with a focus on automated verification.
Currently, my primary interest is verifying parameterized concurrent programs over network topologies: How to represent the topologies and classify them in terms of decidability results? What is the expressivity of the proof methods? How to make proofs compositional? How to turn theoretical results into user-friendly verification tools?
In addition, I have been working on hyperproperty verification.
My email address: chengrt at cs.toronto.edu
Draft
- Symmetric Proofs of Parameterized Programswith Azadeh Farzan
[arXiv]
Publications
- Complete Local Reasoning About Parameterized Programs Over Topologieswith Azadeh Farzan
CAV'26 (Distinguished Paper) [link] [extended version] - Products of Recursive Programs for Hypersafety Verificationwith Azadeh Farzan
OOPSLA'25 [link] [extended version]
Service
- Artifact Evaluation Committee: PLDI 2026, FormaliSE 2025
- Student Volunteer: FLoC 2026
Teaching Assistantships
- CSC410 Software Testing and Verification: Summer 2026 (Prep), Fall 2025
- CSC110/111 Foundations of Computer Science: Summer 2025 (Prep)
- CSC448/2405 Formal Languages and Automata: Winter 2025
- CSC324 Principles of Programming Languages: Fall 2024 (Lead), Winter 2024
- CSC309 Programming on the Web: Fall 2023
Before graduate school
I received H.B.Sc. with high distinction from the University of Toronto in November 2023. During my undergrad, I worked on the following projects:
- Recursive program synthesis, with Dr. Victor Nicolet and Prof. Azadeh Farzan;
- Test concretization in model-based testing, with Dr. Lina Marsso and Dr. Nick Feng.
I also assisted with a research about the use of proof assistants, particularly Lean, in math education, led by Dr. Kitty Yan.
Prior to university, I participated in programming contests and won a silver medal in National Olympiad in Informatics, China, 2017.