Title: Scalable Symbolic Execution

Speaker: Zijiang Yang, Western Michigan University

Time: 10:00, Friday, May 31, 2013

Venue: Meeting Room (A1114), 11rd Floor, Building #5, Institute of Software, Chinese Academy of Sciences

Abstract:

Symbolic execution is emerging as a powerful technique for generating test inputs systematically to achieve exhaustive path coverage of a bounded depth. However, its practical use is often limited by path explosion because the number of paths of a program can be exponential in the number of branch conditions encountered during the execution. To mitigate the path explosion problem, we propose a new redundancy removal method to identify sub paths shared by multiple runs and eliminate them during test generation. Pruning away such redundant paths can lead to a potentially exponential reduction in the number of paths. Our experimental results confirm that redundancy due to common sub paths is both abundant and widespread in real-world applications. In both KLEE and Cloud9, the addition of our new method has led to a speedup of up to two orders of magnitude in the execution time.

Bio:

Dr. Zijiang Yang is an associate professor with tenure in computer science at Western Michigan University, and a visiting professor in the department of electrical engineering and computer science at the University of Michigan. He holds a Ph.D. degree from the University of Pennsylvania, a M.S. degree from Rice University and a B.S. degree from the University of Science and Technology of China, all in computer science.

Dr. Yang’s research interests are in the areas of software systems. The primary focus of his research is to develop formal method based tools to support the modeling, analysis and verification of complex software such as high performance computing programs. His research has been supported by National Science Foundation, Office of Naval Research and several industrial grants. Dr. Yang holds 10 U.S. patents and has published more 50 papers in technical journals and conference proceedings. He received ACM TODAES best paper award in 2008, PADTAD best paper award in 2010, and WMU CEAS Young Researcher Award in 2008. Dr. Yang is a senior member of IEEE.