Yao Peisen 姚培森 Assistant Professor School of Cyber Science and Technology College of Computer Science and Technology Zhejiang University Office: Room 9362, 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 ] [ Students ] [ Misc ]

I am looking for self-motivated students (undergraudate, graudate, ...) to work with. If you are interested, please drop me an email:).

---

News

• I am currently on the program committee of ISSTA 2024 and IEEE EuroS&P 2024. Please consider submitting a paper!
• 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 ensure software reliability, e.g.,

• Program Analysis and Verification
• Program Synthesis and Automated Reasoning

Current Research

• Program Analysis and Verification
  • Path sensitivity [PLDI21'a] [ISSTA'20], context sensitivity (via CFL-reachability) [OOPSLA'22a]
  • Reasoning about concurrency [PLDI21'b] [USENIX Security'23], collections [TOSEM'23], and numerics [OOPSLA'21] [ASE'21] [ICSE'22] [ASE'23a]
  • Fuzz testing (General purpose [S&P'24] [TDSC'23] [S&P'22 ] [S&P'20], domain specific [ESEC/FSE'21] [ISSTA'21])
  • Equivalence verification [ICSE'23] and change impact analysis [ASE'23b] for Fintech systems
• Program Synthesis and Automated Reasoning
  • Synthesis for code optimization [OOPSLA'22b ] and search [ECOOP'23]
  • Synthesizing best transformers for abstract interpretation [OOPSLA'21]
  • A formulation of Pearl’s axioms for causal discovery [ICSE'24]

Selected Publications

• 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
• 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)
• 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)
• Technical Report: Efficient Path-Sensitive Data-Dependence Analysis.
  Peisen Yao, Jinguo Zhou, Xiao Xiao, Qingkai Shi, Rongxin Wu, and Charles Zhang
  

* means corresponding author.

---

Honors & Awards

• Google Research Paper Rewards
  
• Honorable Mention in the CSE Best Dissertation Award, HKUST
  
• ACM SIGPLAN Distinguished Paper Award
  
• Qizhen Scholar of ZJU (浙江大学启真优秀青年学者)
  
• Outstanding Undergraduate Award of HUST
  
• Second Place in HPL track, Asia Super-computing Student Competition (ASC)
  
• Technical Excellence Award, Unique Hackday
  

---

Software

• Program Analysis and Verification

  • 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

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

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

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

• Program Synthesis and Automated Reasoning

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

  • Arlib: A library for playing with various automated reasoning tasks, such as model counting, Optimization Modulo Theory (OMT) solving, etc. ([ISSTA'20] [OOPSLA'21])

---

Service

• Chair or Co-chair: CCF ChinaSoft'23优秀博士生论坛
• Program Committee: SNAER'24 (Demo), IEEE EuroS&P'24, ISSTA'24, SPLASH'23 (SRC), ChinaSoft'23, RAID'23, PLDI'23
• Artifact Evaluation Committee: OOPSLA'24, ICSE'24, PLDI'23, USENIX Security'23, MobiSys'23, ATC'22, OSDI'22
• 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, IEEE Transactions on Reliability, Journal of Software

Mentoring

• Long-term mentor of SIGPLAN-M

Courses

• 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

• Some interesting papers
• Writing a technical paper by Michael Ernst
• Tips on writing a research paper by Tom Reps
• Type and proof (unfinished tutorial)
• Automated reasoning for logics and programs (unfinished...)