Sciweavers

Share
SPIN
2009
Springer

Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis

8 years 10 months ago
Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis
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 th...
Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Cha
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where SPIN
Authors Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Chao Wang
Comments (0)
books