Yao Peisen

Email:

rainoftime - at - gmail - dot- com

pyao - at - connect - dot- ust - dot - hk

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
  Value flow analysis, numerical domains, fuzzing
• Automated Reasoning
  Symbolic abstraction, deductive synthesis

News

• I am currenctly a postdoc research associate in HKUST, and will be joining Zhejiang University as an Assistant Professor this year... 欢迎校内外感兴趣的同学联系~~
• 浙江大学关于2023年接收外校推荐免试研究生工作安排的通知...
• I am currently on the program committee of PLDI 2023. Please consider submitting a paper!

Dissertation

• Solidifying and Scaling SMT-based Program Analysis.
  Ph.D. Dissertation. 2022.
  Committee members: Charles Zhang, Shing-Chi Cheung, Fangzhen Lin, Hongce Zhang, and Darko Marinov (External committee)

Publications

• [OOPSLA 2022] 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) [tool]
• [OOPSLA 2022] 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) [pdf]
• [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) [study data and bug reports] [pdf]
• [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) [pdf]
• [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) [pdf]
• [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)[pdf]
  
• [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) [pdf]
  
• [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) [pdf]
  
• [PLDI 2021] 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) [pdf]
  
• [PLDI 2021] 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) [pdf]
  
• [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) [pdf]
  
• [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) [pdf]
  

* means corresponding author.

Drafts/Technical Reports

• Anchor: Fast and Precise Value-Flow Analysis for Containers via Memory Orientation. Chengpeng Wang, Wenyang Wang, Peisen Yao, Qingkai Shi, Jinguo Zhou, and Charles Zhang. Under revision
• Efficient Path-Sensitive Data-Dependence Analysis. Peisen Yao, Jinguo Zhou, Xiao Xiao, Qingkai Shi, Rongxin Wu, and Charles Zhang.
• Duplicate-sensitivity Guided Transformation Synthesis for DBMS Correctness Bug Detection. Yushan Zhang, Peisen Yao, Rongxin Wu, and Charles Zhang.

Projects

• Static Analysis, Static Vulnerability Detection

  Pinpoint/Fusion is an industrial-strength next-generation automated bug finding tool through static analysis (PLDI'21a, PLDI'21b, ASE'21, ICSE'22, OOPSLA'22). It has found 500+ bugs in many mature and fundamental open-source projects, including HBase, Apache, MySQL, Firefox, Git, Python, memcached, OpenSSL, redis, tmux, Vim, Mariadb, and many others.

• Dynamic Vulnerability Analysis, Fuzz Testing

  Fuzz testing is an automated software testing technique that is conducted to reveal coding errors and security loopholes. We are interested in leveraging our static analysis knowledge to optimize fuzz testers (S&P'20, S&P'22) (a partial of vulnerabilities can be found here), and applying fuzz testers to domain-specific application scenarios. Specificaly, the SMTFuzz framework (ESEC/FSE'21, ISSTA'21) 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, ATC'22 (artifact evaluation), OSDI'22 (artifact evaluation)
  
• Reviewer/Sub-/Co-reviewer: ATVA'22, ISSRE'21, ESEC/FSE'19, ISSTA'19, ASE'18, VMCAI'17
  

Teaching

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

Invited Talks

• Introduction to Metamorphic Testing (蜕变测试导引), System Security Summer School, Zhejiang University
  
• Solidifying and Scaling SMT-based Program Analysis, Nanjing Univeristy
  
• Scaling and Solidifying SMT-based Program Analysis, Shanghai Jiao Tong University
  

Misc

• Some interesting papers
  
• Writing a technical paper by Michael Ernst
  
• Tips on writing a research paper by Tom Reps