Zhonghan Wang

zhece.wang@mail.utoronto.ca

I am a Ph.D. student in Electrical and Computer Engineering at The Edward S. Rogers Sr. Department of Electrical and Computer Engineering of the University of Toronto. Earlier, I earned my B.Eng (2021) in Electrical Engineering from Nankai University, and M.Eng (2025) in Institute of Software, Chinese Academy of Sciences.

My research focuses on formal methods, automated reasoning, and AI-assisted verification, including three key research themes:

1. Investigate advanced techniques in SMT solving and nonlinear arithmetic, including clause-level decision strategies for NLSAT, local search optimization for nonlinear real arithmetic, and improving solver efficiency on SMT-LIB benchmarks.
2. Formal verification of distributed protocols and concurrent systems, involving model checking, symbolic reasoning, and automated consistency verification to ensure correctness and reliability in large-scale distributed applications.
3. Explore formal methods for AI and LLMs, such as integrating theorem proving with large language models to enhance reasoning capabilities, verify logical consistency, and assist in automated theorem proving tasks.

CV  |  Google Scholar  |  LinkedIn  |  Github  |  ORCID  |  Blog