Ti Zhou

Ph.D. candidate
Department of Computer Science
Stony Brook University (SBU)

Email: tizhou1 at cs dot stonybrook dot edu
Ti Zhou

I'm a CS PhD candidate at Stony Brook University (since Fall 2023), advised by Prof. Shuai Mu. My research is about making formal reasoning practical, in two directions: designing novel formal abstractions that bring real, high-performance systems within reach of verification; and using formal methods and symbolic reasoning to build AI agents that are both more capable and more efficient.

Before joining Stony Brook, I completed my M.Sc. (2023) and Honours B.Sc. (2021) in Computer Science at StFX University in Canada, where I was advised by Prof. Man Lin. I worked on designing and implementing reinforcement learning agents that run inside the Linux kernel for energy-efficient CPU frequency management.

I enjoy many forms of art, and I see computer systems as one of them. I do some painting.

Industry Experience

Applied Scientist Intern
Amazon AWS Security · 2026 – present
Formal-methods-driven evaluation of system code changes.

Selected Publications

Lion: Modular Verification of Async Runtime Liveness
T. Zhou, Z. Zhang, O. Chowdhury and S. Mu.
SOSP 2026. (62/390, 15.9% acceptance rate)ACM Artifacts Available badgeACM Artifacts Evaluated — Functional badgeACM Results Reproduced badge
Async runtime Logical Log abstraction Attaches to general system shapes Specifies both safety and liveness
[PDF][Artifact: Lion async runtime]
AutoMan: Facilitating Verified Distributed Systems Development Through Automatic Code Generation and Manual Optimizations
Z. Zhang*, T. Zhou* (* co-1st authors), C. Jenkins, O. Chowdhury and S. Mu.
SOSP 2025. (65/368, 17.7% acceptance rate)ACM Artifacts Available badgeACM Artifacts Evaluated — Functional badgeACM Results Reproduced badge
Spec-to-implementation recovery DSL/transpilation/code generation Refinement-based verification
[PDF][Artifact: AutoMan transpiler]
CPU Frequency Scheduling of Real-Time Applications on Embedded Devices with Temporal Encoding-based Deep Reinforcement Learning
T. Zhou and M. Lin.
Journal of Systems Architecture, 2023.
Neuro-symbolic system In-kernel agent
[PDF] [Artifact: Neural Network in Linux kernel] [A Linux Contribution] [Profiling CPU power management in Linux] [A follow-up work scales the method to multiple tasks]

Students Mentored

Yitong Zhao 2024 – 2025 · High School → Undergrad@UIUC

Xinyi Li 2022 – 2024 · Undergrad@StFX → PhD@Dalhousie

Haoyu Wang 2022 – 2024 · Undergrad@StFX → PhD@Dalhousie

I designed and led projects based on my M.Sc. thesis for Xinyi [PDF] and Haoyu [PDF], each of which led to a publication in IEEE Trans. on Sustainable Computing.