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

---

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

I am looking for self-motivated Ph.D. and master students (enrolled in 2025)! Please read this if you are a student interested in working with me (e.g., for Ph.D., Master, RA/intern, and Bachelor's thesis).

---

News

• I am currently on the program committee of POPL 2025, ISSTA 2025, ISSTA 2024 and CCS 2024. Please consider submitting a paper!
• Our paper on fast and precise buffer overflow detection has been accepted by ISSTA'24!
• Our paper "Verifying Data Constraint Equivalence in FinTech Systems" has been accepted at ICSE 2023! The equivalence verifier has been deployed in Ant Group (a global FinTech company with 1 billion activeusers), and is available on GitHub!
• BEACON (S&P'22) is selected for Google Research Paper Rewards!
• Our paper "Complexity-Guided Container Replacement Synthesis (OOPSLA'22)" has been recognized with an ACM SIGPLAN Distinguished Paper Award!
• Lockpick has been accepted at USENIX Security'23. It uncovers 203 unique and confirmed lock misuses from a broad spectrum of impactful systems, including OpenSSL, Linux Kernel, PostgreSQL, MariaDB, FFmpeg, Apache HTTPd, and FreeBSD.

---

Research Interests

I am broadly interested in topics related to programming languages, software engineering, and cybersecurity, with an emphasis on using program reasoning techniques to make software secure, usable, and fast.

Current Research

• Program Analysis and Verification
  • Automated verification for artificial intelligence [ICSE'24]
  • Path sensitivity [PLDI'24][PLDI21'a] [ISSTA'20], context sensitivity (via CFL-reachability) [OOPSLA'22a]
  • Reasoning about concurrency [PLDI21'b] [USENIX Security'23], memory [TOSEM'23] [ISSTA'24], numerics [OOPSLA'21] [ASE'21] [ICSE'22] [ASE'23a], change impacts [ASE'23b], and DSL [ICSE'23]
  • Fuzz testing: general purpose [S&P'24] [TDSC'23] [ S&P'22 ] [S&P'20], domain specific [ESEC/FSE'21] [ ISSTA'21]
• Program Synthesis and Automated Reasoning
  • Program synthesis for code optimization [OOPSLA'22b ], search [ECOOP'23], and translation [ASPLOS'24]
  • Symbolic abstraction: application in synthesizing best abstract transformers [OOPSLA'21]

Selected Publications

• 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)
• TOSEM 24: 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)

* means corresponding author.

---

Honors & Awards

• NSFC Excellent Young Scientists Program (Overseas) 国家高层次青年人才计划
  
• Google Research Paper Rewards
  
• ACM SIGPLAN Distinguished Paper Award
  
• Qizhen Scholar of ZJU (浙江大学启真优秀青年学者)
  
• Honorable Mention in the CSE Best Dissertation Award, HKUST
  
• Outstanding Undergraduate Award, HUST
  
• Second Place in Linpack track, ASC
  
• Technical Excellence Award, Unique Hackday
  

---

Software

• Current Projects

  • canary: A program analysis and verification framework (alias analysis, SMT solving, ...)

  • efmc: An SMT-based software model checker (ASE'23a)

  • arlib: A library for playing with various automated reasoning tasks, such as model counting, Optimization Modulo Theory (OMT) solving, etc.


• Former Projects

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

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

  • Pangolin: A fuzzing framework (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
    • We received the Google Research Paper Rewards and two Huawei Distinguished Collaborator Awards for deploying our fuzzers
    • Beacon is available here

  • EqDAC: An equivalence checker for verifying data constraint equivalence (ICSE'23)

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

  • Cres: Program synthesis for code optimization [OOPSLA'22b ] and code search [ECOOP'23]

  • smtfuzz: A fuzz testing tool for SMT solvers (ESEC/FSE'21, ISSTA'21)

    • smtfuzz has found hundreds of 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"

---

Service

• Chair or Co-chair: CCF ChinaSoft'23优秀博士生论坛
• Technical Program Committee: POPL'25 (first PC from ZJU:), ISSTA'25, CCS'24, EuroS&P'24, ISSTA'24, RAID'23, PLDI'23 (first PC from ZJU:), ChinaSoft'24(形式化方法与应用论坛), ChinaSoft'23(形式化方法与应用论坛)
• Artifact Evaluation Committee: PLDI'24, OOPSLA'24, ICSE'24, PLDI'23, USENIX Security'23, MobiSys'23, ATC'22, OSDI'22
• Program Committee of other Tracks: SNAER'24 (Demo), OOPSLA'23 (SRC)
• Conference Reviewer/Sub-reviewer/Co-reviewer: ATVA'22, ISSRE'21, ESEC/FSE'19, ISSTA'19, ASE'18, VMCAI'17
• Journal Reviewer: ACM Transactions on Programming Languages and Systems, ACM Transactions on Knowledge Discovery from Data, IEEE Transactions on Reliability, 电子学报，软件学报，计算机学报

Mentoring

• Long-term mentor of SIGPLAN-M

---

Teaching

• Principles of Compilers (Spring 2024), ZJU.
• 信息安全前沿技术和研究方法论. 研究生课程，软件分析与形式化方法部分(3学时) (Spring 2023, Spring 2024), ZJU.
• COMP4632: Practicing CyberSecurity: Attacks and Counter-measures, Teaching Assistant, HKUST
• COMP3021: Java Programming, Teaching Assistant, HKUST
• COMP3511: Operating System, Teaching Assistant, HKUST

---

Students

• Students

---

Misc

• Tips on writing a research paper by Thomas Reps
• Writing a technical paper by Michael Ernst
• Doing research in software analysis: lessons and tips by Zhendong Su
• Some interesting papers
• Automated reasoning for logic and programs