Name
Title | ||
|---|---|---|
Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis |
Abstract | ||
|---|---|---|
While symmetry reduction has been established to be an important technique for reducing the search space in model checking, its application in concurrent software verification is still limited, due to the difficulty of specifying symmetry in realistic software. We propose an algorithm for automatically discovering and applying transition symmetry in multithreaded programs during dynamic model checking. Our main idea is using dynamic program analysis to identify a permutation of variables and labels of the program that entails syntactic equivalence among the residual code of threads and to check whether the local states of threads are equivalent under the permutation. The new transition symmetry discovery algorithm can bring substantial state space savings during dynamic verification of concurrent programs. We have implemented the new algorithm in the dynamic model checker Inspect . Our preliminary experiments show that this algorithm can successfully discover transition symmetries that are hard or otherwise cumbersome to identify manually, and can significantly reduce the model checking time while using Inspect to examine realistic multithreaded applications. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-02652-2_22 | SPIN |
Keywords | Field | DocType |
dynamic model checker,dynamic model checking,dynamic analysis,transition symmetry,dynamic program analysis,dynamic verification,new transition symmetry discovery,new algorithm,model checking time,multithreaded programs,automatic discovery,model checking,symmetry reduction,software verification,search space,state space | Model checking,Computer science,Permutation,Thread (computing),Theoretical computer science,Software,Equivalence (measure theory),State space,Dynamic program analysis,Software verification | Conference |
Volume | ISSN | Citations |
5578 | 0302-9743 | 15 |
PageRank | References | Authors |
0.62 | 23 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yu Yang | 1 | 121 | 5.95 |
| Xiaofang Chen | 2 | 15 | 0.62 |
| Ganesh Gopalakrishnan | 3 | 1619 | 130.11 |
| Chao Wang | 4 | 1109 | 61.81 |