Combining Symmetry Reduction with Generalized Symbolic Trajectory Evaluation
Y. Li, N. Zeng, William N. N. Hung, Xiaodong Song · The Computer Journal · 2013
This paper combines symmetry reduction with generalized symbolic trajectory evaluation (GSTE) to tackle state explosion. The inherent correlation between structure symmetry and property symmetry is formalized as a theorem, which provides the soundness of our symmetry reduction method. We introduce a practical strategy to effectively integrate the symmetry-reduction approach in a hybrid verification environment which combines theorem proving and GSTE. The effectiveness of our method is demonstrated by case studies.