Title
Using unfoldings in automated testing of multithreaded programs
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önen1293.07
Olli Saarikivi2477.43
Keijo Heljanko375147.90