Peisen Yao Assistant Professor · ZJU 100 Young Professor School of Cyber Science and Technology College of Computer Science and Technology Zhejiang University Office: Room 311, Tower B06, ZJU-Hangzhou Global Scientific and Technological Innovation Center Office*: Room 216, Shaw Business Administration Building, Yuquan Campus EmailZJU Profile

News

• I am looking for self-motivated students! Please read this if you are interested in working with me (e.g., for Ph.D., Master, SRTP, and FYP).
• Our work "SIMD-Accelerated Sparse Bit-Vectors for Pointer Analysis" has been accepted at ASE 2026!
• pyflow has been released on PyPI as pyflow-analysis! Check it out with pip install pyflow-analysis.
• aria has been released on PyPI as pyaria! Check it out with pip install pyaria.
• We have released lotus, a versatile and industrial-scale program analysis and verification framework (SPLASH/ISSTA'26 Demo, CAV'26, ASE'26, TOSEM'26a, ISSTA'25, S&P'24, USENIX Security'23, TSE'24, OOPSLA'22)
• I am currently on the program committee of FSE 2027. Please consider submitting a paper!

---

Research Interests

I am broadly interested in programming languages, software engineering, and cybersecurity, focusing on techniques that make software fast, reliable, and secure.

Selected projects and research themes (current and former):

• Program Analysis and Verification
  
  • Path-sensitive analysis: [TOSEM'26b] [PLDI'24] [TOSEM'24] [PLDI'21a]
  • Alias analysis: [arxiv:2608.04466][SPLASH/ISSTA'26 Demo] [ASE'26] [PLDI'24] [ISSTA'24 ] [TOSEM'23] [OOPSLA'22a]
  • Numerical analysis: [TOSEM'26b] [ISSTA'25] [ASE'23a] [ICSE'22] [ASE'21]
  • Concurrency analysis: [USENIX Security'23] [PLDI'21b]
  • Symbolic abstraction: [measuring precision] [parallel symbolic abstraction] [OOPSLA'21]
  • Fuzzing: directed [S&P'24] [S&P'22 ], hybrid [S&P'20], scheduling [TDSC'23], and testing solvers [SAS'25] [ESEC/FSE'21] [ISSTA'21]
• Program Synthesis and Optimization
  
  • Synthesizing Datalog [ECOOP'23] and code translators [TOSEM'25] [ASPLOS'24]
  • Optimizing compiler hints [Findings of ACL'26], Java collections [OOPSLA'22b ], and database-backed applications [ICSE'23]
• Logic and Automated Reasoning
  
  • Satisfiability solving: [string constraints] [shared-context batched SAT] [TOSEM'26a] [ISSTA'20]
  • Symbolic automata and extended regular expressions: [complexity of SemREs] [CAV'26]

---

Manuscripts / Working Papers

• PyFlow: An Inter-procedural Static Analysis Framework for Python. Zinan Gu, Haoxiang Yan, and Peisen Yao.
• Accelerating C/C++ Pointer Analysis via Compiler-Based Offline Simplifications [preprint]. Zinan Gu, Peisen Yao, and Kui Ren
• Learning Splitting Heuristics for Parallel String Solvers [preprint]. Chenhao Gao and Peisen Yao.
• Shared-Context Batched Satisfiability for Constraint-Based Program Analysis[preprint]. Jiening Siow, Hanrui Zuo, Hanyun Jiang, Weiqi Wang, and Peisen Yao.
• A Fresh Look at Best Inductive Loop Invariant Synthesis for Bit-Vector Relations [preprint]. Hanrui Zuo, Peisen Yao, and Kui Ren.
• Synthesizing Best Abstract Transformers via Parallel Bit-Vector Optimization [preprint]. Weiqi Wang, Peisen Yao, Hanrui Zuo, Yuan Li, Hongfei Fu, and Kui Ren.

---

Selected Publications

• [SPLASH/ISSTA'26 Demo] Phoenix: A Modular and Versatile Framework for C/C++ Pointer Analysis.
  Peisen Yao*, Zinan Gu, and Qingkai Shi.
  Tool Demonstration Track, Joint Conference of ISSTA and SPLASH (SPLASH/ISSTA 2026)
• [ASE 2026] SIMD-Accelerated Sparse Bit-Vectors for Pointer Analysis.
  Zhaoyang Tan, Peisen Yao*, and Kui Ren.
  The 41st IEEE/ACM International Conference on Automated Software Engineering.
• [TOSEM 2026b] Path-Sensitive Loop Invariant Inference via Large Language Models and Abstract Interpretation.
  Guangsheng Fan, Liqian Chen, Peisen Yao, Banghu Yin, Wenyu Zhang, and Ji Wang.
  ACM Transactions on Software Engineering and Methodology.
• [CAV 2026] Sound and Precise Symbolic Automata Model for Stateful Software Systems.
  Xinlong Wu, Ruiyu Zhou, Peisen Yao, and Qingkai Shi.
  The 38th International Conference on Computer Aided Verification.
• [Findings of ACL 2026] HintPilot: LLM-Based Compiler Hint Synthesis for Code Optimization.
  Hanyun Jiang, Peisen Yao*, Kaiyue Li, Tingting Lin, Chengpeng Wang, and Kui Ren.
  Findings of the Association for Computational Linguistics.
• [TOSEM 2026a] Compiler Optimizations-Based SMT Simplifications: An In-Depth Study.
  Hanyun Jiang, Peisen Yao*, Jiachen Lu, Yongwang Zhao, and Kui Ren.
  ACM Transactions on Software Engineering and Methodology.
  Accpeted by the Journal First track of FSE 2026.
• [SAS 2025] Bounded-Exhaustive Subspace Diversification for SMT Solver Testing.
  Junda Zheng and Peisen Yao*.
  The 32nd Static Analysis Symposium.
• [ISSTA 2025] Program Analysis Combining Generalized Bit-Level and Word-Level Abstractions.
  Guangsheng Fan, Liqian Chen, Banghu Yin, Wenyu Zhang, Peisen Yao, and Ji Wang.
  The ACM SIGSOFT International Symposium on Software Testing and Analysis.
• [FSE 2025] Understanding Industry Perspectives of Static Application Security Testing (SAST) Evaluations.
  Yuan Li, Peisen Yao*, Kan Yu, Chengpeng Wang, Yaoyang Ye, Song Li, Meng Luo, Yepang Liu, Kui Ren.
  The ACM International Conference on the Foundations of Software Engineering.
• [TOSEM 2025] KBX: Verified Model Synchronization via Formal Bidirectional Transformation.
  Jianhong Zhao, Yongwang Zhao, Peisen Yao, Fanlang Zeng, Bohua Zhan, and Kui Ren.
  ACM Transactions on Software Engineering and Methodology.
• [PLDI 2024] Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis.
  Peisen Yao, Jinguo Zhou, Xiao Xiao, Qingkai Shi, Rongxin Wu, and Charles Zhang.
  The ACM SIGPLAN Conference on Programming Language Design and Implementation.
  The first PLDI paper from ZJU!
• [ASPLOS 2024] SIRO: Empowering Version Compatibility in Intermediate Representations via Program Synthesis.
  Bowen Zhang, Wei Chen, Peisen Yao, Chengpeng Wang, Wensheng Tang, and Charles Zhang.
  ACM International Conference on Architectural Support for Programming Languages and Operating Systems.
• [ISSTA 2024] Precise Compositional Buffer Overflow Detection via Heap Disjointness.
  Yiyuan Guo, Peisen Yao*, and Charles Zhang.
  The ACM SIGSOFT International Symposium on Software Testing and Analysis.
  ACM SIGSOFT Distinguished Paper Award.
• [TOSEM 2024] Octopus: Scaling Value-Flow Analysis via Parallel Collection of Realizable Path Conditions.
  Wensheng Tang, Dejun Dong, Shijie Li, Chengpeng Wang, Peisen Yao, Jinguo Zhou, and Charles Zhang.
  ACM Transactions on Software Engineering and Methodology.
• [ICSE 2024] Enabling Runtime Verification of Causal Discovery Algorithms with Automated Conditional Independence Reasoning.
  Pingchuan Ma, Zhenlan Ji, Peisen Yao, Shuai Wang, and Kui Ren.
  The 2024 IEEE/ACM International Conference on Software Engineering.
• [S&P 2024] Titan: Efficient Multi-Target Directed Greybox Fuzzing.
  Heqing Huang, Peisen Yao*, Hung-Chun Chiu, Yiyuan Guo, and Charles Zhang.
  The 45th IEEE Symposium on Security and Privacy (Oakland).
• [ASE 2023a] Demystifying Template-Based Invariant Generation for Bit-Vector Programs.
  Peisen Yao, Jingyu Ke, Jiahui Sun, Hongfei Fu, Rongxin Wu, and Kui Ren.
  The 2023 IEEE/ACM Automated Software Engineering Conference.
• [ASE 2023b] DCLink: Bridging Data Constraint Changes and Implementations in FinTech Systems.
  Wensheng Tang, Chengpeng Wang, Peisen Yao, Rongxin Wu, Xianjin Fu, Gang Fan, and Charles Zhang.
  The 2023 IEEE/ACM Automated Software Engineering Conference.
• [ECOOP 2023] Synthesizing Conjunctive Queries for Code Search.
  Chengpeng Wang, Peisen Yao*, Wensheng Tang, Gang Fan, and Charles Zhang.
  European Conference on Object-Oriented Programming.
• [TDSC 2023] Balance Seed Scheduling via Monte Carlo Planning.
  Heqing Huang, Hung-Chun Chiu, Qingkai Shi, Peisen Yao, and Charles Zhang.
  IEEE Transactions on Dependable and Secure Computing.
• [ICSE 2023] Verifying Data Constraint Equivalence in FinTech Systems.
  Chengpeng Wang, Gang Fan, Peisen Yao*, Fuxiong Pan, and Charles Zhang.
  The 2023 IEEE/ACM International Conference on Software Engineering.
• [USENIX Security 2023] Place Your Locks Well: Understanding and Detecting Lock Misuse Bugs.
  Yuandao Cai, Peisen Yao*, Chengfeng Ye, and Charles Zhang.
  The 32nd USENIX Security Symposium.
• [TOSEM 2023] Anchor: Fast and Precise Value-Flow Analysis for Containers via Memory Orientation.
  Chengpeng Wang, Wenyang Wang, Peisen Yao*, Qingkai Shi, Jinguo Zhou, Xiao Xiao, and Charles Zhang.
  ACM Transactions on Software Engineering and Methodology.
• [OOPSLA 2022a] Indexing the Extended Dyck-CFL Reachability for Context-Sensitive Program Analysis.
  Qingkai Shi, Yongchao Wang, Peisen Yao, and Charles Zhang.
  The 37th ACM SIGPLAN Conference on Objected Oriented Programming, Systems, Languages, and Applications.
• [OOPSLA 2022b] Complexity-Guided Container Replacement Synthesis.
  Chengpeng Wang, Peisen Yao*, Wensheng Tang, Qingkai Shi, and Charles Zhang.
  The 37th ACM SIGPLAN Conference on Objected Oriented Programming, Systems, Languages, and Applications.
  ACM SIGPLAN Distinguished Paper Award.
• [ICSE 2022] Precise Divide-by-Zero Detection with Affirmative Evidence.
  Yiyuan Guo, Jinguo Zhou, Peisen Yao*, Qingkai Shi, and Charles Zhang.
  The 2022 IEEE/ACM International Conference on Software Engineering.
• [S&P 2022] BEACON: Directed Grey-Box Fuzzing with Provable Path Pruning.
  Heqing Huang, Yiyuan Guo, Qingkai Shi, Peisen Yao, Rongxin Wu, and Charles Zhang.
  The 43rd IEEE Symposium on Security and Privacy (Oakland).
  Google Research Paper Rewards.
• PhD Thesis: Solidifying and Scaling SMT-Based Program Analysis, 2022, HKUST.
  Honorable Mention in the CSE Best Dissertation Award, HKUST.
• [OOPSLA 2021] Program Analysis via Efficient Symbolic Abstraction.
  Peisen Yao, Qingkai Shi, Heqing Huang, and Charles Zhang.
  The 36th ACM SIGPLAN Conference on Objected Oriented Programming, Systems, Languages, and Applications.
  (One of the algorithms has been integrated into SVF).
• [ASE 2021] Transcode: Detecting Status Code Mapping Errors in Large-Scale Systems.
  Wensheng Tang, Yikun Hu, Gang Fan, Peisen Yao, Rongxin Wu, Guangyuan Bai, Pengcheng Wang, and Charles. Zhang
  The 2021 IEEE/ACM Automated Software Engineering Conference.
• [ESEC/FSE 2021] Skeletal Approximation Enumeration for SMT Solver Testing.
  Peisen Yao, Heqing Huang, Wensheng Tang, Qingkai Shi, Rongxin Wu, and Charles Zhang.
  The ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering.
• [ISSTA 2021] Fuzzing SMT Solvers via Two-Dimensional Input Space Exploration.
  Peisen Yao, Heqing Huang, Wensheng Tang, Qingkai Shi, Rongxin Wu, and Charles Zhang.
  The 30th ACM SIGSOFT International Symposium on Software Testing and Analysis.
• [PLDI 2021a] Path-Sensitive Sparse Analysis without Path Conditions.
  Qingkai Shi, Peisen Yao, Rongxin Wu, and Charles Zhang.
  The 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation.
• [PLDI 2021b] Canary: Practical Static Detection of Inter-Thread Value-Flow Bugs.
  Yuandao Cai, Peisen Yao, and Charles Zhang.
  The 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation.
• [ISSTA 2020] Fast Bit-Vector Satisfiability.
  Peisen Yao, Qingkai Shi, Heqing Huang, and Charles Zhang.
  The 29th ACM SIGSOFT International Symposium on Software Testing and Analysis.
• [S&P 2020] Pangolin: Incremental Hybrid Fuzzing with Polyhedral Path Abstraction.
  Heqing Huang, Peisen Yao, Rongxin Wu, Qingkai Shi, and Charles Zhang.
  The 41st IEEE Symposium on Security and Privacy (Oakland).

---

Honors & Awards

• Third-place in the single-query tracks of OF_ABV, QF_AUFBV, and QF_BVFP, SMT-COMP 2025
• ACM SIGSOFT Distinguished Paper Award (ISSTA 2024)
• CCF-Huawei Innovation Research Award (2023-formal method, 2024-compilers)
• NSFC Excellent Young Scientists Program (Overseas) 国家高层次青年人才计划
• Google Research Paper Rewards, 2022
• ACM SIGPLAN Distinguished Paper Award (OOPSLA 2022)
• Qizhen Scholar of ZJU (浙江大学启真优秀青年学者)
• Honorable Mention in the CSE Best Dissertation Award, HKUST, 2022
• Huawei Distinguished Collaborator, 2021
• Outstanding Undergraduate Award, HUST
• Second Place in Linpack Track (We broke the world record!), ASC 2014
• Technical Excellence Award, Unique Hackday

---

Software

• Current Projects

  • lotus is a program analysis and verification framework built on top of LLVM, CUDD, WALI, Z3, and Crab (SPLASH/ISSTA'26 Demo, CAV'26, ASE'26, TOSEM'26a, ISSTA'25, S&P'24, USENIX Security'23, TSE'24, OOPSLA'22)

  • pyflow is a static analysis framework for Python, featuring shape analysis, IFDS dataflow analysis, and beyond, with applications in security checking and program optimization. It is also available on PyPI — try pip install pyflow-analysis!

  • aria is a library for automated reasoning and program verification. (ICSE'24, ICSE'23, ASE'23) It is also available on PyPI — try pip install pyaria!

  • and more...

• Former Projects

  • Pinpoint is an SMT-based, industrial-strength static analysis framework (PLDI'24, ECOOP'23, TOSEM'23, USENIX Security'23, OOPSLA'22b , OOPSLA'22a, ICSE'22, ASE'21, PLDI'21b, PLDI'21a...)
    

    • Pinpoint has found hundreds of bugs in many mature and fundamental open-source projects, including Linux Kernel, FreeBSD, Firefox, HBase, OpenSSL, PostgreSQL, MySQL, Memcached, Redis, FFmpeg, Apache HTTPd, Git, Python, Tmux, Vim, and many others
    • Pinpoint was commercialized at Sourcebrella Inc, which was acquired by Ant Group

  • Pangolin is a fuzzer for C/C++ source code and binaries (Pangolin S&P'20, Beacon S&P'22, BeliefFuzz TDSC'23, Titan S&P'24)

    • A partial of of detected vulnerabilities in open-source projects can be found here
    • Our work has been successfully deployed in the Huawei tool-chain and detected more than 1000+ bugs! We have thus received the Huawei Distinguished Collaborator 2021 award

  • smtfuzz is a fuzzer for SMT solvers (SAS'25, ESEC/FSE'21, ISSTA'21)

    • Smtfuzz has found 1000+ bugs in several state-of-the-art SMT solvers and first-order theorem provers, such as Z3, CVC5, Yices2, STP, Boolector, MathSAT5, SMTInterpol, OpenSMT, SMT-RAT, DReal, SPASS, and Vampire
    • You may try a simplified implementation of the random formula generator by "pip install smtfuzz"

  • EqDAC is an equivalence checker for verifying data constraint equivalence (ICSE'23)

    • EqDAC has been deployed in Ant Group, a global FinTech company with 1 billion active users

---

Service

• Chair/Co-chair/Organizer
  • CCF ChinaSoft'26 约束求解技术与应用论坛
  • FM Meets AI长三角系列活动（杭州站）
  • CCF ChinaSoft'25 软件分析与软件安全新技术论坛
  • CCF ChinaSoft'23 优秀博士生论坛
• Technical Program Committee
  • POPL: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2025) (first PC from ZJU)
  • PLDI: ACM SIGPLAN Conference on Programming Language Design and Implementation (2026, 2023) (first PC from ZJU)
  • OOPSLA: ACM SIGPLAN Conference on Objected Oriented Programming, Systems, Languages, and Application (2025) (first PC from ZJU)
  • FSE: ACM International Conference on the Foundations of Software Engineering (2027)
  • ISSTA: ACM SIGSOFT International Symposium on Software Testing and Analysis (2026, 2025, 2024)
  • ASE: IEEE/ACM Automated Software Engineering Conference (2026, 2025)
  • SAS: International Static Analysis Symposium (2025)
  • CCS: ACM Conference on Computer and Communications Security (2025, 2024)
  • ACSAC: The Annual Computer Security Applications Conference (2026, 2025)
  • EuroS&P: IEEE European Symposium on Security and Privacy (2024)
  • RAID: International Symposium on Research in Attacks, Intrusions and Defenses (2023)
  • SETTA: Symposium on Dependable Software Engineering. Theories, Tools and Applications (2024)
  • CCF ChinaSoft (2025, 2024, 2023)
  • National Conference of Theoretical Computer Science (2026, 2025)
• Reviewer Committee Member
  • ACM TOSEM: ACM Transactions on Software Engineering and Methodology (Jan 2026 – Dec 2027)
• Journal Reviewer
  • ACM TOPLAS: ACM Transactions on Programming Languages and Systems
  • ACM TOSEM: ACM Transactions on Software Engineering and Methodology
  • IEEE TSE: IEEE Transactions on Software Engineering
  • EMSE: Empirical Software Engineering
  • IEEE TDSC: IEEE Transactions on Dependable and Secure Computing
  • ACM TOPS: ACM Transactions on Privacy and Security
  • ACM TKDD: ACM Transactions on Knowledge Discovery from Data
  • IEEE TR: IEEE Transactions on Reliability
  • 电子学报，软件学报，计算机学报
• Program Committee of other Tracks: OOPSLA'26 (LMPL), OOPSLA'25 (LMPL), ASE'24 (Industry), OOPSLA'23 (SRC)
• Artifact Evaluation Committee: PLDI (2024, 2023), OOPSLA (2024), ICSE (2024), USENIX Security (2023), ATC (2022), OSDI (2022)
• External Reviewer/Sub-reviewer/Co-reviewer: OOPSLA'26, ATVA'22, ISSRE'21, ESEC/FSE'19, ISSTA'19, ASE'18, VMCAI'17

---

Teaching

• Principles of Programming Languages (Spring 27), UG Course, ZJU
• Compiler Construction (Spring 26, 25, 24), UG Course, ZJU
• 信息安全前沿技术和研究方法论, 研究生课程 (26, 25, 24, 23), 软件分析&&形式化方法部分, ZJU
• COMP4632: Practicing CyberSecurity: Attacks and Counter-measures, Teaching Assistant, HKUST
• COMP3021: Java Programming, Teaching Assistant, HKUST
• COMP3511: Operating System, Teaching Assistant, HKUST

---

Misc

• Tips on writing a research paper by Thomas Reps [video]
• Writing a technical paper by Michael Ernst
• Doing research in software analysis: lessons and tips by Zhendong Su
• Some interesting papers
• Lecture notes on compiler construction (ing...)
• Lecture notes on principles of programming languages (ing...)
• Automated reasoning for logic and programs (ing...)
• CVE: A list of CVE identifiers for vulnerabilities discovered through our research

Invited Talks

• Agentic Code Optimization. 编译前沿技术论坛, CNCC (中国计算机大会). 2026.10
• Fast and Precise Abstract Interpretation, ChinaSoft 编程语言前沿技术论坛论坛, 2025.11
• Optimization Modulo Theories (OMT) Solving for Program Analysis, ChinaSoft 青年学者论坛, 2025.11
• Optimization Modulo Theories (OMT) Solving for Program Analysis, HCP'25, 2025.08
• Optimization Modulo Theories (OMT) Solving for Program Analysis, ISCAS, 2024.11
• Program Analysis via Symbolic Abstraction, Shanghai Jiao Tong University, 2024.06
• Program Analysis via Symbolic Abstraction, Nanjing University, 2023.12
• Program Analysis via Symbolic Abstraction, CCF Young Computer Scientists & Engineers Forum, 2023.11
• Program Analysis via Symbolic Abstraction, HCP'23 (第六届难解问题的表示、算法与应用研讨会), 2023.07
• 高精度静态数值缺陷分析, CCF ChinaSoft'22 高可信嵌入式软件工程技术论坛，2022.11
• Complexity-Guided Container Replacement Synthesis, CCF ChinaSoft'22 顶会顶刊论坛, 2022.11
• Program Analysis via Symbolic Abstraction [slide], SIG-Program Analysis, 2022.10
• Introduction to Metamorphic Testing [slide], System Security Summer School, Zhejiang University
• Solidifying and Scaling SMT-based Program Analysis, Xiamen University
• Solidifying and Scaling SMT-based Program Analysis, Nanjing University
• Scaling and Solidifying SMT-based Program Analysis, Shanghai Jiao Tong University
• Scaling and Solidifying SMT-based Program Analysis, ShanghaiTech University

---