08:30 - 09:00

• DASE: Document-Assisted Symbolic Execution for Improving Automated Software Testing

  We propose and implement a new approach, Document-Assisted Symbolic Execution (DASE), to improve automated test generation and bug detection. DASE leverages natural language processing techniques and heuristics to analyze program documentation to extract input constraints automatically. DASE then uses the input constraints to guide symbolic execution to focus on inputs that are semantically more important. We evaluated DASE on 88 programs from 5 mature real-world software suites: COREUTILS, FINDUTILS, GREP, BINUTILS, and ELFTOOLCHAIN. DASE detected 12 previously unknown bugs that symbolic execution without input constraints failed to detect, 6 of which have already been confirmed by the developers.

   

  Preprint available: 

Edmund Wong; Lei Zhang; Song Wang; Taiyue Liu; Lin Tan

University of Waterloo, Canada

09:00 - 09:30

• Compositional Symbolic Execution with Memoized Replay

  Symbolic execution is a powerful, systematic analysis that has received much visibility in the last decade. Scalability however remains a major challenge for symbolic execution. Compositional analysis is a well-known general purpose methodology for increasing scalability. This paper introduces a new approach for compositional symbolic execution. Our key insight is that we can summarize each analyzed method as a memoization tree that captures the crucial elements of symbolic execution, and leverage these memoization trees to efficiently replay the symbolic execution of the corresponding methods with respect to their calling contexts. Memoization trees offer a natural way to compose in the presence of heap operations, which cannot be dealt with by previous work that uses logical formulas as summaries for compositional symbolic execution. Our approach also enables efficient target oriented symbolic execution for error detection or program coverage. Initial experimental evaluation based on a prototype implementation in Symbolic Path Finder shows that our approach can be up to an order of magnitude faster than traditional non-compositional symbolic execution.

Rui Qiu; Guowei Yang; Corina S. Pasareanu; Sarfraz Khurshid

The University of Texas at Austin, USA; Texas State University, USA; CMU, USA; NASA Ames Research Center, USA

09:30 - 10:00 

• Regular Property Guided Dynamic Symbolic Execution

  A challenging problem in software engineering is to check if a program has an execution path satisfying a regular property. We propose a novel method of dynamic symbolic execution (DSE) to automatically find a path of a program satisfying a regular property. What makes our method distinct is when exploring the path space, DSE is guided by the synergy of static analysis and dynamic analysis to find a target path as soon as possible. We have implemented our guided DSE method for Java programs based on JPF and WALA, and applied it to 13 real-world open source Java programs, a total of 225K lines of code, for extensive experiments. The results show the effectiveness, efficiency, feasibility and scalability of the method. Compared with the pure DSE on the time to find the first target path, the average speedup of the guided DSE is more than 258X when analyzing the programs that have more than 100 paths.

   

  Preprint available: 

Yufeng Zhang; Zhenbang Chen; Ji Wang; Wei Dong; Zhiming Liu

National University of Defense Technology, China; Birmingham City University, UK

10:00 - 10:30 

• Combining Symbolic Execution and Model Checking for Data Flow Testing

  Data flow testing (DFT) focuses on the flow of data through a program. Despite its higher fault-detection ability over other structural testing techniques, practical DFT remains a significant challenge. This paper tackles this challenge by introducing a hybrid DFT framework: (1) The core of our framework is based on dynamic symbolic execution (DSE), enhanced with a novel guided path search to improve testing performance, and (2) we systematically cast the DFT problem as reach ability checking in software model checking to complement our DSE-based approach, yielding a practical hybrid DFT technique that combines the two approaches' respective strengths. Evaluated on both open source and industrial programs, our DSE-based approach improves DFT performance by 60~80% in terms of testing time compared with state-of-the-art search strategies, while our combined technique further reduces 40% testing time and improves data-flow coverage by 20% by eliminating infeasible test objectives. This combined approach also enables the cross-checking of each component for reliable and robust testing results.

Ting Su; Zhoulai Fu; Geguang Pu; Jifeng He; Zhendong Su

East China Normal University, China; University of California at Davis, USA