CV
Curriculum Vitae
Contact Information
| Name | Xinyu Zhang |
| Professional Title | Ph.D. Student in Software Engineering |
| westtide##stu.ecnu.edu.cn | |
| Location | Shanghai, China |
Professional Summary
Researcher in formal methods, focusing on model checking, constrained Horn clause solving, and program verification.
Education
-
2025 - Present Shanghai, China
Ph.D. Student
East China Normal University
Software Engineering
- Research focus: model checking and CHC solving.
- Advisor: Prof. Jianwen Li.
-
2022 - 2025 Guangzhou, China
M.Eng.
Guangzhou University
Cyberspace Security
- Research focus: Loop Invariant Synthesis.
- Advisor: Prof. Hanpin Wang.
-
2016 - 2021 Chengdu, China
B.Eng.
Southwest Jiaotong University
Network Engineering
- Research focus: modeling and formal verification in railway control systems.
- Advisor: Associate Prof. Keming Wang.
Projects
-
Formal Verification of openHiTLS Cryptographic Algorithms (SM3/SM4) via Frama-C
OSPP advanced topic.
- Completed end-to-end integration between openHiTLS and Frama-C.
- Built a formal verification pipeline for SM3 and SM4 algorithms.
- Resolved tool adaptation and interface compatibility issues to improve engineering reliability.
-
Master's Thesis: Program-Semantics-Guided Loop Invariant Synthesis
Research thesis project.
-
Undergraduate Thesis: Modeling and Verification of a CBTC Zone Controller with Atelier B
Research thesis project.
Skills
Formal Methods: Z3 (SAT/SMT/CHC), Model Checking (IC3/PDR), Loop Invariant, CBMC
Common Tools: GCC, Bash, Docker, LLM Prompting
Programming Languages: Python, C++, LaTeX
Languages
Chinese : Native
Wu dialect : Native
English : IELTS 6.5
Honors and Awards
-
2025 Outstanding Graduate of Guangzhou University
-
2024 University of Macau Exchange Program in Cyberspace Security and Computer Science - Best Presentation
-
2023 OSPP Advanced Topic - Cross-System Performance Tuning Tool
Contributions: PR1.
-
2022 Guangzhou University Graduate Academic Scholarship - First Prize
-
2018 15th May Day Mathematical Modeling Contest - First Prize