Software bugs cost developers and software companies a great deal of time and money. To tame such beasts hidden in software, developers from the industry use various static and dynamic analysis tools to check possible bugs. Over the past two decades, Satisfiability modulo theories (SMT) solving has become a critical part of many program analyses, such as symbolic execution and refinement type checking.
 
My research tackles the challenges of improving the scalability and reliability of SMT-based program analysis. In the first part of the talk, I will present our work for improving the scalability of SMT-based hybrid fuzzing and path-sensitive sparse analysis, respectively. The proposed techniques have been deployed in many global 500 companies and have reported hundreds of new bugs. In the second part of the talk, I will show a general,  principled, and practical approach for finding bugs in SMT solvers. Our work has detected over 1000 confirmed bugs in several state-of-the-art solvers, such as Z3, CVC4, Yices2, Boolector, and OpenSMT.

Peisen Yao is a Ph.D. candidate at The Hong Kong University of Science and Technology. His research areas are software engineering, programming language, and cybersecurity, with a focus on using program analysis techniques to ensure software reliability. He has published at premium venues of software engineering (FSE, ASE, ISSTA), programming languages (PLDI, OOPSLA), and cybersecurity (S&P). His research has led to over a thousand software vulnerabilities in open-source software and has been successfully commercialized.