Abstraction-Guided Hybrid Symbolic Execution for Testing Concurrent Systems

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.

Speaker Details

Neha Rungta is a PhD candidate at Brigham Young University. Her adviser is Dr. Eric Mercer. Research has focused on heuristics for guided search, randomized search techniques, and benchmarking criteria for explicit state model checking and symbolic execution. Awarded the Google Anita Borg Scholarship in 2007. Developed a guided test framework for the Java Pathfinder model checker as part of Google Summer of Code 2008.

Date:
Speakers:
Neha Rungta
Affiliation:
Brigham Young University