Abstract | ||
---|---|---|
In multithreaded programs both environment input data and the nondeterministic interleavings of concurrent events can affect the behavior of the program. One approach to systematically explore the nondeterminism caused by input data is dynamic symbolic execution. For testing multithreaded programs we present a new approach that combines dynamic symbolic execution with unfoldings, a method originally developed for Petri nets but also applied to many other models of concurrency. We provide an experimental comparison of our new approach with existing algorithms combining dynamic symbolic execution and partial-order reductions and show that the new algorithm can explore the reachable control states of each thread with a significantly smaller number of test runs. In some cases the reduction to the number of test runs can be even exponential allowing programs with long test executions or hard-to-solve constrains generated by symbolic execution to be tested more efficiently. |
Year | DOI | Venue |
---|---|---|
2012 | 10.1145/2351676.2351698 | ASE |
Keywords | DocType | ISSN |
nondeterministic interleaving,program testing,partial-order reduction,symbolic execution,petri nets,concurrency control,dynamic symbolic execution,input data,smaller number,long test execution,test run,multi-threading,multithreaded program,concurrency model,program behavior,unfoldings,test execution,automated testing,new approach,unfoldings method,new algorithm,environment input data,multi threading,partial order reduction,petri net | Conference | 1527-1366 |
ISBN | Citations | PageRank |
978-1-4503-1204-2 | 12 | 0.61 |
References | Authors | |
9 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Kari Kähkönen | 1 | 29 | 3.07 |
Olli Saarikivi | 2 | 47 | 7.43 |
Keijo Heljanko | 3 | 751 | 47.90 |