Abstraction-Guided Hybrid Symbolic Execution for Testing Concurrent Systems

Опубликовано 6 сентября 2016, 18:29

The paradigm shift from inherently sequential to highly concurrent and multi-threaded applications is creating new challenges for testers and verification engineers. In this work we present an abstraction-guided hybrid symbolic execution technique to check the reachability of certain target locations. The input target locations are generated from static analysis warnings or user-specified reachability properties. We generate an abstract system that contains program locations relevant for checking the reachability of the target locations. We guide a hybrid symbolic program execution (data input values are represented symbolically while other values are concrete) along paths in the abstract system in order to generate a corresponding feasible execution trace. We use a combination of heuristics for ranking thread and data non-determinism to guide the execution. An empirical analysis demonstrates that abstract traces can quickly be concretized to find concurrency errors using the guided hybrid symbolic execution technique where exhaustive search techniques fail.