Xinyu Zhang

I am Xinyu Zhang, a Ph.D. student in Software Engineering at East China Normal University in Shanghai.

My research lies at the intersection of Formal Methods and Artificial Intelligence. I focus on model checking, constrained Horn clause solving, and program verification, with recent work on LLM-assisted formal reasoning.

I previously received my M.Eng. in Cyberspace Security from Guangzhou University, where I worked on program-semantics-guided loop invariant synthesis, and my B.Eng. in Network Engineering from Southwest Jiaotong University.

Outside research, I enjoy resistance training and hiking.

---

Research Interests

• Model Checking: IC3/PDR, CAR, BMC
• SAT, SMT, CHC
• Program Verification： Frama-c (ACSL), CBMC
• AI4FM, FM4AI