Ting Su (ECNU)

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 reachability 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.