Zhe Zhou (周喆)

LWSN 3133 (#55) · Purdue University, West Lafayette, IN 47907 · zhou956@purdue.edu

I am a postdoctoral researcher at Purdue University, working with Prof. Suresh Jagannathan. I received my Ph.D. in Computer Science from Purdue University, where I was advised by Prof. Suresh Jagannathan and Prof. Benjamin Delaware. Prior to my doctoral studies, I worked as a full-time software engineer at Megvii (Face++) from 2017 to 2018. I earned my bachelor's degree from Peking University in 2017, where I was advised by Prof. Guangyu Sun.

My research focuses on formal methods, with particular on formal verification and property-based testing for complex systems software. I develop automated verification techniques to establish deep semantic correctness guarantees for complex systems software---beyond basic crash safety or memory safety. My current work explores how AI tools (e.g., LLMs) can strengthen automated verification and complicate property (e.g., liveness and reachability property) reasoning for distributed systems and concurrent programs. I am also interested in the intersection of machine learning (ML) and PL—both applying ML techniques to formal methods problems and using formal methods insights to enhance ML.

Here is my CV.


Publications

Trace-Guided Synthesis of Effectful Test Generators

Zhe Zhou, Ankush Desai, Benjamin Delaware, and Suresh Jagannathan

(PLDI 2026) ACM SIGPLAN Conference on Programming Language Design and Implementation

(Conditional Accepted)

Polymorphic Coverage Types

Zhe Zhou, Ashish Mishra, Benjamin Delaware, and Suresh Jagannathan

(JFP 2026) Journal of Functional Programming

(Minor Revision)

We've Got You Covered: Type-Guided Repair of Incomplete Input Generators

Patrick LaFontaine, Zhe Zhou, Ashish Misra, Suresh Jagannathan, and Benjamin Delaware

(OOPSLA 2025) ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications

(full version) (artifact)

Derivative-Guided Symbolic Execution

Yongwei Yuan, Zhe Zhou, Julia Belyakova, and Suresh Jagannathan

(POPL 2025) Proceedings of the ACM on Programming Languages

(doi) (full version) (artifact)

A HAT Trick: Automatically Verifying Representation Invariants Using Symbolic Finite Automata

Zhe Zhou, Qianchuan Ye, Benjamin Delaware, and Suresh Jagannathan

(PLDI 2024) ACM SIGPLAN Conference on Programming Language Design and Implementation

(doi) (draft) (full version) (artifact)

Covering All the Bases: Type-Based Verification of Test Input Generators

Zhe Zhou, Ashish Mishra, Benjamin Delaware, and Suresh Jagannathan

(PLDI 2023) ACM SIGPLAN Conference on Programming Language Design and Implementation

(Distinguished Paper Award) (doi) (draft) (full version) (artifact)

Data-Driven Abductive Inference of Library Specifications

Zhe Zhou, Robert Dickerson, Benjamin Delaware, and Suresh Jagannathan

(OOPSLA 2021) ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications

(Distinguished Artifact Award) (doi) (full version) (artifact) (talk)