Yao Peisen 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, Zhejiang University Email: pyaoaa@zju.edu.cn Official homepage at ZJU: https://person.zju.edu.cn/pyao

---

[ Publications ] [ Awards ] [ Software ] [ Service ] [ Teaching ] [ Students ] [ Misc ]

---

News

• I am looking for self-motivated students (enrolled in 2026)! Please read this if you are interested in working with me (e.g., for Ph.D., Master, SRTP, and FYP).
• smtfuzz v0.1.1 is released! This release includes new mutation engines, parallel runner support, and additional enhancements.
• I am currently on the program committee of PLDI 2026, ASE 2025, CCS 2025, and OOPSLA 2025. Please consider submitting a paper!

---

Research Interests

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

Current Research

• Program Analysis and Verification
  • Path sensitivity [TOSEM'24] [PLDI'21a] [ISSTA'20], context sensitivity (via CFL-reachability) [OOPSLA'22a]
  • Alias analysis [PLDI'24] [ISSTA'24 ] [TOSEM'23] [OOPSLA'22a]
  • Numerical analysis [ISSTA'25] [ASE'23a] [ICSE'22] [OOPSLA'21] [ASE'21]
  • Concurrency analysis [USENIX Security'23] [PLDI21'b], change impact analysis [ASE'23b]
  • Fuzzing: directed [S&P'24] [S&P'22 ], sheduling [TDSC'23], hybrid [S&P'20], oracle [ESEC/FSE'21], configurations [ISSTA'21]
• Program Synthesis and Optimizations
  • Program synthesis for code search [ECOOP'23] and translation [TOSEM'25] [ASPLOS'24]
  • Optimizations of Java collections [OOPSLA'22b ] and database-backed applications [ICSE'23]
• Logic and Automted Reasoning
  • Symbolic abstraction [OOPSLA'21]
  • A formalization of conditional independence [ICSE'24]

---

Manuscripts

• Sythesizing Best Inductive Invariants. Hanrui Zuo, Peisen Yao, and Kui Ren. Working paper.
• Parallelizing Symbolic Abstraction. Weiqi Wang, Peisen Yao, Yuan Li, Hanrui Zuo, Hongfei Fu, and Kui Ren. Working paper.
• Learning to Solve String Constraints. Chenghao Gao, Peisen Yao, and Kui Ren. Working paper.
• Boosting Compiler Optimization-Based SMT Simplifications. Hanyun Jiang, Peisen Yao, Jiachen Lu, Yongwang Zhao, and Kui Ren. Working paper.

---

Selected Publications

• SAS 2025: Bounded-Exhaustive Subspace Diversification for SMT Solver Testing
  Junda Zheng and Peisen Yao.
  The 32nd Static Analysis Symposium (CCF Rank B)
• 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 (CCF Rank A)
• 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 (CCF Rank A)
• 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 (CCF Rank A)
• 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 (CCF Rank A)
  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 (CCF Rank A)
• 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 (CCF Rank A)
  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 (CCF Rank A)
• 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 (CCF Rank A)
• 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) (CCF Rank A)
• 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 (CCF Rank A)
• 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 (CCF Rank A)
• 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 (CCF Rank B)
• 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 (CCF Rank A)
• 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 (CCF Rank A)
• 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 (CCF Rank A)
• 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 (CCF Rank A)
• 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 (CCF Rank A)
• 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 (CCF Rank A)
  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 (CCF Rank A)
• 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) (CCF Rank A)
  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 (CCF Rank A)
  (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 (CCF Rank A)
• 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 (CCF Rank A)
• 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 (CCF Rank A)
• 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 (CCF Rank A)
• 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 (CCF Rank A)
• 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 (CCF Rank A)
• 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) (CCF Rank A)

---

Honors & Awards

• 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 (ISSTA'25)

  • efmc is an SMT-based software model checker with several engines, including template-based verification, Houdini, k-induction, IC3/PDR, etc. (ASE'23a)

  • arlib is a library for playing with various automated reasoning tasks, such as model counting, quantifier elimination, etc (ICSE'24, ICSE'23)

  • 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"

• Former Projects

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

    • 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

  • 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

  • Cres is a program synthesizer for code optimization [OOPSLA'22b ] and code search [ECOOP'23]

---

Service

• Chair/Co-chair/Organizer
  • 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)
  • ISSTA: ACM SIGSOFT International Symposium on Software Testing and Analysis (2025, 2024)
  • ASE: IEEE/ACM Automated Software Engineering Conference (2025)
  • SAS: International Static Analysis Symposium (2025)
  • CCS: ACM Conference on Computer and Communications Security (2025, 2024)
  • ACSAC: The Annual Computer Security Applications Conference (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 (2025)

• 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
  • 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'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)
• Conference Reviewer/Sub-reviewer/Co-reviewer: ATVA'22, ISSRE'21, ESEC/FSE'19, ISSTA'19, ASE'18, VMCAI'17

---

Teaching

• Principles of Programming Languages (Spring 2026), UG Course, ZJU
• Compiler Construction (Spring 2024, 2025, 2026), UG Course, ZJU
• 信息安全前沿技术和研究方法论, 研究生课程 (2023, 2024, 2025), 软件分析&&形式化方法部分, 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