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

---

[Research Interests] [Publications] [Software] [Service] [Students] [Misc]

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

---

News

• 浙江大学计算机科学与技术学院关于接收2023级推荐免试研究生工作安排的通知...
• 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.)
• I am currently on the program committee of PLDI 2023. Please consider submitting a paper.

---

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
  
• Automated Reasoning
  

Current Research Projects

• Static Program Analysis
  
  • Path sensitivity: [TOSEM'23] [PLDI21'a] [ISSTA'20]
    
  • Context sensitivity (via CFL-reachability): [OOPSLA'22a]
  • Best abstraction in abstract interpretation: [OOPSLA'21]
  • Concurrecny: [PLDI21'b]
• Vulnerability Scanning
  
• Static Bug Finding: [USENIX Security'23] [ICSE'22] [ASE'21]
  
• Fuzz Testing: [S&P'22] [ESEC/FSE'21] [ISSTA'21] [S&P'20]
  
• Program Synthesis / Repair: [OOPSLA'22b]
  

---

Publications

• 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)
  
• 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 (CCF Rank A)
  
• 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.
  
• 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 (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.

---

Software

• Static Analysis, Static Vulnerability Detection

  • Pinpoint/Fusion: an industrial-strength next-generation automated bug finding tool through static analysis (PLDI'21b, ASE'21, ICSE'22, OOPSLA'22a, TOSEM'23). It has found 300+ bugs in many mature and fundamental open-source projects, including Linux Kernel, MySQL, Firefox, HBase, Apache, Git, Python, Memcached, OpenSSL, Redis, Tmux, Vim, Mariadb, and many others.

  • Canary and Lockpick: a static analysis framework for concurrent programs (PLDI'21a, USENIX Security'23). It uncovers 200+ unique and confirmed concurrency bugs (dead locks, double locking, concurrent UAF, etc) from a broad spectrum of impactful systems, including OpenSSL, Linux Kernel, PostgreSQL, MariaDB, FFmpeg, Apache HTTPd, and FreeBSD.

• Dynamic Analysis, Fuzz Testing

  • Pangolin and Beacon: static analysis guided hybrid fuzzing (S&P'20, depolyed in Huawei) and directed greybox fuzzing (S&P'22, available at dockerhub). A partial of detected vulnerabilities can be found here.

  • SMTFuzz: a framework for testing/fuzzing SMT sovlers (ESEC/FSE'21, ISSTA'21), which 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.

• Automated Program Verification, Model Checking

  To appear...

---

Service

• Program Committee: PLDI'23, ChinaSoft'22
  
• Artifact Evaluation Committee: PLDI'23, USENIX Security'23, ATC'22, OSDI'22
  
• Conference Reviewer/Sub-/Co-reviewer: ATVA'22, ISSRE'21, ESEC/FSE'19, ISSTA'19, ASE'18, VMCAI'17
  
• Journal Reviewer: IEEE Transactions on Reliability, Journal of Software
  

Mentoring

• Long-term mentor of SIGPLAN-M
  

Courses

• COMP4632: Practicing CyberSecurity: Attacks and Counter-measures
  
• COMP3021: Java Programming
  
• COMP3511: Operating System
  

---

Invited Talks

• 高精度静态数值缺陷分析, CCF ChinaSoft'22 高可信嵌入式软件工程技术论坛， Nov 2022
  
• Complexity-Guided Container Replacement Synthesis, CCF ChinaSoft'22 顶会顶刊论坛, Nov 2022
  
• Program Analysis via Symbolic Abstraction (基于符号抽象的程序分析), SIG-程序分析, Oct 2022
  
• Introduction to Metamorphic Testing (蜕变测试导引), System Security Summer School, Zhejiang University
  
• Solidifying and Scaling SMT-based Program Analysis, Xiamen University
  
• Solidifying and Scaling SMT-based Program Analysis, Nanjing Univeristy
  
• Scaling and Solidifying SMT-based Program Analysis, Shanghai Jiao Tong University
  
• Scaling and Solidifying SMT-based Program Analysis, ShanghaiTech University
  

---

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