Efficient testing of concurrent programs with abstraction-guided symbolic execution
Date
2009
Authors
Rungta N.
Mercer E.G.
Visser W.
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
In this work we present an abstraction-guided symbolic execution technique that quickly detects errors in concurrent programs. The input to the technique is a set of target locations that represent a possible error in the program. We generate an abstract system from a backward slice for each target location. The backward slice contains program locations relevant in testing the reachability of the target locations. The backward slice only considers sequential execution and does not capture any inter-thread dependencies. A combination of heuristics are to guide a symbolic execution along locations in the abstract system in an effort to generate a corresponding feasible execution trace to the target locations. When the symbolic execution is unable to make progress, we refine the abstraction by adding locations to handle inter-thread dependencies. We demonstrate empirically that abstraction-guided symbolic execution generates feasible execution paths in the actual system to find concurrency errors in a few seconds where exhaustive symbolic execution fails to find the same errors in an hour. © 2009 Springer Berlin Heidelberg.
Description
Keywords
Abstract systems, Actual system, Concurrency errors, Concurrent program, Execution paths, Execution trace, Reachability, Sequential execution, Symbolic execution, Target location, Abstracting, Computer software, Errors, Location, Spin dynamics, Targets, Model checking
Citation
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
5578 LNCS
5578 LNCS