Abstract: Symbolic execution is a precise program analysis method for systematically exploring a program's path space. In principle, symbolic execution is powered and also challenged by constraint solving. However, we observe that symbolic execution mainly utilizes the constraint solver in a black-box manner. On the other hand, constraint solvers also do not specifically consider their application scenarios. Hence, we argue that we can synergize symbolic execution and constraint solving more tightly to improve symbolic execution's efficiency and effectiveness further.
In this talk, I will introduce our recent progress on this high-level idea. On the one side, we utilize more information inside constraint solvers to improve symbolic execution. On the other side, we also pass the information collected or inferred during symbolic execution to the constraint solver for improving solving's efficiency. As a result, we expect to have symbolic execution-oriented constraint solvers in the future.
Bio: Zhenbang Chen is an associate professor of the College of Computer, National University of Defense Technology, China. He obtained his Ph.D. degree from the National University of Defense Technology in 2009. His current research interests include program analysis, formal methods, and their applications.
腾讯会议 ID：509 708 733
会议链接：https://meeting.tencent.com/dm/90yzzVFsA4Xn
